ertes 2017-02-10 19:45:14
aarvar: this one does exist: data Foo a r = Nil r | Cons a (Foo a r) -- note the flipped type arguments
ertes 2017-02-10 19:45:32
aarvar: one version of it is pipes' Producer a Identity r
ertes 2017-02-10 19:45:42
aarvar: another version is Free ((,) a) r
ertes 2017-02-10 19:46:06
and there are probably more
mniip 2017-02-10 20:03:40
hmm
mniip 2017-02-10 20:03:45
all types are profunctors
c_wraith 2017-02-10 20:06:47
in what category?
mniip 2017-02-10 20:07:31
Hask^op x Hask -> Hask, I believe
mniip 2017-02-10 20:07:53
maybe something more interesting in presence of HKTs
c_wraith 2017-02-10 20:08:30
Err. I don't think types are even objects in that category
mniip 2017-02-10 20:08:36
well
mniip 2017-02-10 20:08:52
(Hask^n)^op x Hask^n -> Hask
mniip 2017-02-10 20:09:01
where n is the number of free variables in the type
mniip 2017-02-10 20:11:57
e.g
ertes 2017-02-10 20:12:12
mniip: so Bool : 1^op × 1 -> Hask?
mniip 2017-02-10 20:12:26
yeah
mniip 2017-02-10 20:12:40
namely the profunctor that selects Bool
ertes 2017-02-10 20:12:47
let 2 = 1 + 1 -- how many free variables?
mniip 2017-02-10 20:12:48
I'm talking about things more like
mniip 2017-02-10 20:13:11
[a] would be the profunctor \(X', X) -> List(X)
mniip 2017-02-10 20:13:28
and then forall a. [a] would be the end (over X) of that
mniip 2017-02-10 20:13:34
and that end is isomorphic to ()
ertes 2017-02-10 20:13:36
do you really mean free variables?
ertes 2017-02-10 20:15:31
data Bool2 = True2 () | False2 () -- is that one or two free variables?
mniip 2017-02-10 20:15:49
0
ertes 2017-02-10 20:16:12
and [] has one?
mniip 2017-02-10 20:16:18
:t []
lambdabot 2017-02-10 20:16:20
[t]
ertes 2017-02-10 20:16:29
[], the type
mniip 2017-02-10 20:16:38
[] isn't a concrete type
ertes 2017-02-10 20:16:47
ah, now i see what you mean
mniip 2017-02-10 20:17:03
I mean types with free variables
mniip 2017-02-10 20:17:09
can be represented with profunctors
mniip 2017-02-10 20:17:14
and then forall-bindings are just ends
ertes 2017-02-10 20:17:27
so Either a b : (Hask^2)^op × Hask^2 -> Hask
mniip 2017-02-10 20:17:32
yes
ertes 2017-02-10 20:18:02
yeah, now it makes sense… not sure if it's an actual profunctor, but i get the idea =)
mniip 2017-02-10 20:18:37
everything is a profunctor
mniip 2017-02-10 20:19:26
the datatype P a = P (F a) (G a)
mniip 2017-02-10 20:19:50
is \(A', A) -> (F(A', A), G(A', A))
mniip 2017-02-10 20:20:06
S a = L (F a) | R (G a)
mniip 2017-02-10 20:20:21
is \(A', A) -> F(A', A) + G(A', A)
mniip 2017-02-10 20:20:29
H a = H (F a -> G a)
mniip 2017-02-10 20:20:43
is \(A', A) -> Hom(F(A, A'), G(A', A))
mniip 2017-02-10 20:20:51
note the flipped arguments
mniip 2017-02-10 20:21:20
oh yeah
mniip 2017-02-10 20:21:26
Identity = \(A', A) -> A
lyxia 2017-02-10 20:21:33
(->) a b ?
ertes 2017-02-10 20:22:21
\((A', B'), (A, B)) -> Hom(A, B)?
lyxia 2017-02-10 20:22:27
oh I can deduce it with F c = a, G c = b...
mniip 2017-02-10 20:22:57
Hom(A', B)
mniip 2017-02-10 20:23:26
the intuition is that every free variable gets 2 arguments: one for contravariant appearances and the other for covariant
lyxia 2017-02-10 20:24:00
Yeah.
mniip 2017-02-10 20:24:10
then
mniip 2017-02-10 20:24:25
forall a. F a -> End_A F(A, A)
aluminumtubes 2017-02-10 20:27:24
what's the difference between a = ((<) 3) and a = (< 3) ?
mniip 2017-02-10 20:27:43
(< 3) is \x -> x < 3
ertes 2017-02-10 20:27:44
aluminumtubes: (< 3) = \x -> x < 3
mniip 2017-02-10 20:27:59
((<) 3) is \x -> (<) 3 x
mniip 2017-02-10 20:28:01
aka 3 < x
mniip 2017-02-10 20:28:24
compare with
mniip 2017-02-10 20:28:28
> (/ 2) 5
ertes 2017-02-10 20:28:29
aluminumtubes: just like (3 /) is dividing 3 by, and (/ 3) is dividing by 3
lambdabot 2017-02-10 20:28:31
2.5
ertes 2017-02-10 20:28:32
hehe
mniip 2017-02-10 20:28:33
> ((/) 2) 5
lambdabot 2017-02-10 20:28:36
0.4
lyxia 2017-02-10 20:29:26
> let a = ((<) 3) in [(b, a b) | b <- [2.5, 2.6 .. 3.5]]
lambdabot 2017-02-10 20:29:29
[(2.5,False),(2.6,False),(2.7,False),(2.8000000000000003,False),(2.900000000...
lyxia 2017-02-10 20:29:33
pffff
ertes 2017-02-10 20:29:50
> let a = ((<) 3) in [(b, a b) | b <- [2.5, 2.75 .. 3.5]]
lambdabot 2017-02-10 20:29:52
[(2.5,False),(2.75,False),(3.0,False),(3.25,True),(3.5,True)]
aluminumtubes 2017-02-10 20:30:20
cool
aluminumtubes 2017-02-10 20:30:27
thanks you guys are awesome
ertes 2017-02-10 20:30:52
use rationals with a power-of-2 denominator to avoid rounding errors
