ski 2017-02-22 07:45:44
in the latter case, we say that if the argument has type `[a]', for some type `a', then `length' can be applied to that, and the result has type `Int'
ski 2017-02-22 07:45:47
mbrock : ok ?
mbrock 2017-02-22 07:48:34
so it kind of relates to the notion of a polymorphic value versus a function that works on polymorphic values
mbrock 2017-02-22 07:48:56
I don't know if you would call (exists a. [a]) a polymorphic value though
ski 2017-02-22 07:49:06
i wouldn't
ski 2017-02-22 07:49:19
i'd perhaps call it an "abstract/opaque value"
mbrock 2017-02-22 07:49:25
okay, yeah
nitrix 2017-02-22 07:49:28
I'd word it differently as "if the function can work for all types `a`, surely we can also say there exists a type `a` such that this function works for it".
ski 2017-02-22 07:49:33
it's hiding some choice of `a' inside it
byorgey 2017-02-22 07:49:38
I'd call it a "natural number"
ski 2017-02-22 07:49:48
nitrix : *nod*
nitrix 2017-02-22 07:50:00
mbrock: The two are synonymous.
nitrix 2017-02-22 07:50:12
(Well in that context)
ski 2017-02-22 07:50:58
`(exists a. ..a..) -> ...' means the same as `forall a. (..a.. -> ...)', while otoh `(forall a. ..a..) -> ...' is something different, closely related to `... -> (exists a. ..a..)' (`frob' above)
mbrock 2017-02-22 07:51:02
how's about ``length :: (forall a. [a]) -> Int''?
mbrock 2017-02-22 07:51:30
I guess that's a very strange type
dolio 2017-02-22 07:51:42
srhb: Oh, I know why. MonoLocalBinds doesn't just make local bindings monomorphic. It makes certain sorts of local bindings monomorphic.
jle` 2017-02-22 07:51:43
doesn't sound like a very useful type either
ski 2017-02-22 07:51:45
mbrock : so you should understand now how LHC allowed `exists' in argument type positions : namely by implementing `(exists a. ..a..) -> ...' as `forall a. (..a.. -> ...)', plain polymorphism
jle` 2017-02-22 07:51:47
*useful function
mbrock 2017-02-22 07:51:50
because the only value of forall a. [a] is [], right?
ski 2017-02-22 07:52:00
yep
ski 2017-02-22 07:52:05
(apart from partial values)
dolio 2017-02-22 07:52:26
srhb: And `bar = _` is nice enough to be generalized.
ski 2017-02-22 07:53:09
mbrock : you might also note that if we think in terms of type-passing. iow the `id = /\a. \(x : a). x' thing. then the difference between `forall a. (..a.. -> ...)' and `(exists a. ..a..) -> ...' is "currying"
mbrock 2017-02-22 07:53:15
is this `exists a. ...a...' equivalence with `forall a. (...a... -> ...)' also a logical tautology?
nitrix 2017-02-22 07:53:33
mbrock: Yeah now you're explicitly saying that the first argument of `length` must be a list whose values can be any type.
ski 2017-02-22 07:53:45
mbrock : in the latter, we take a pair of a type `a', and a value of type `..a..' as argument. in the former, we first take a type `a', and return a function that takes a value of type `..a..'
mbrock 2017-02-22 07:53:45
eh, `exists a. ...a... -> ...'
ski 2017-02-22 07:54:19
mbrock : if you meant `(exists a. ...a...) -> ...', then yes. it's a logical tautology (holding both classically and intuitionistically)
dolio 2017-02-22 07:54:24
ski: I think LHC allows exists anywhere, but you can't constrain the quantified types.
ski 2017-02-22 07:55:08
mbrock : otoh, the similar logical equivalence between `(forall a. ..a..) -> ...' and `exists a. (..a.. -> ...)' only holds classically, not constructively/intuitionistically
nitrix 2017-02-22 07:55:17
mbrock: [42, "hi", True]. Normally lists are homogeneous in Haskell because there's not anything useful you can do with `[forall a. a]` other than the length of the list.
ski 2017-02-22 07:55:51
mbrock : the difference in terms of computation is that in the latter case, we have picked a single type `a', while in the former (rank-two) case, we can use the polymorphic argument as many times as we like, and so pick many different `a's
reactormonk 2017-02-22 07:56:08
In ghci, what's a way to unlift an Either in ghci? Aka Right a -> a
nitrix 2017-02-22 07:56:19
ski: My bad.
nitrix 2017-02-22 07:56:21
I was.
jle` 2017-02-22 07:56:30
reactormonk: you can pattern match
ski 2017-02-22 07:56:44
dolio : ok. news to me. ty
reactormonk 2017-02-22 07:56:47
jle`, I've tried Either foo <- ...
reactormonk 2017-02-22 07:56:56
Ehh Right foo
jle` 2017-02-22 07:57:06
Right foo <- return bar
nitrix 2017-02-22 07:57:07
ski: It gets confusing quickly when you're reading other messages too x]
jle` 2017-02-22 07:57:08
should work
jle` 2017-02-22 07:57:14
or let Right foo = bar
nitrix 2017-02-22 07:57:16
ski: I'll let you handle it.
jle` 2017-02-22 07:57:29
the second one probably is less silly
reactormonk 2017-02-22 07:57:31
jle`, yeah, was let. Thanks.
ski 2017-02-22 07:57:53
mbrock : shall i continue ?
dolio 2017-02-22 07:57:58
ski: I'm not 100% sure. But just putting it in argument position wouldn't be very interesting. :)
ski 2017-02-22 07:58:05
dolio : .. exactly :)
ski 2017-02-22 07:58:24
dolio : mostly useful for type synonyms
ski 2017-02-22 07:58:48
dolio : .. someone (i realized) was wanting `exists' in constraint type synonyms here, a few hours ago
dolio 2017-02-22 07:59:17
Yeah, that's another level beyond what they don't support.
ski 2017-02-22 08:00:20
to be able to abbreivate `forall a b. (Foo a,Bar a b) => ..b..' as `forall b. FooBar b => ..b..', with `type FooBar b = exists a. (Foo a,Bar a b)'
dolio 2017-02-22 08:01:50
Oh, I see. That'd be somewhat more feasible, I suppose.
mbrock 2017-02-22 08:01:54
my specific desire comes from using lens-ish "HasFoo", "HasBar" classes for record fields, in combination with parametricity, to be very specific about which part of a state record is needed for a particular function
ski 2017-02-22 08:01:54
shouldn't be harder than `exists' in argument type positions, from what i see
ski 2017-02-22 08:01:55
(oh, perhaps that someone was mbrock .. i've already forgotten :)
mbrock 2017-02-22 08:02:00
and then wanting to abbreviate common combinations of fields, and combine those combinations too
mbrock 2017-02-22 08:02:04
yeah (:
mbrock 2017-02-22 08:03:19
like ``type HasMonsterHealth s = (HasMonster s monster, HasHealth monster Int)''
mbrock 2017-02-22 08:03:48
which would be written ``type HasMonsterHealth s = exists monster. (Has Monster s monster, HasHealth monster Int)''
ski 2017-02-22 08:03:59
(would need FDs to not be ambiguous, though, i think)
ski 2017-02-22 08:04:42
(and then, maybe, it would be nicer to use associated types ?)
dolio 2017-02-22 08:05:41
Yeah, possibly.
ski 2017-02-22 08:06:09
mbrock : do you want me to go on, now ?
mbrock 2017-02-22 08:06:52
ski: yes!
ski 2017-02-22 08:07:25
mbrock : ok. so i explained the producer/consumer duality for `forall a. ..a..' and `exists a. ..a..'
ski 2017-02-22 08:08:23
mbrock : nitrix hinted at stuff like `[exists a. ..a..]', and i could go on with some discussion of how that differs from `exists a. [..a..]'. and similarly how `forall a. IO (Blah a)' differs from `IO (forall a. Blah a)'
ski 2017-02-22 08:09:06
mbrock : but, first at least, i wanted to explain `.. => ..' vs. `.. *> ..' (the latter also being non-existing, conceptual syntax)
ski 2017-02-22 08:10:06
mbrock : to consume a value of type `C a => Foo a', you must provide evidence for `C a' (for the particular `a' that's in scope). to produce it, you may freely *assume* `C a' holds
reactormonk 2017-02-22 08:10:39
With parsec, is there a way to call it similar to Read?
ski 2017-02-22 08:11:18
mbrock : typically (but not always) `=>' is used together with an immediately preceeding `forall', like `forall m t. MonadState (StateBlah t) m => ..m..' perhaps
reactormonk 2017-02-22 08:11:58
aka `parseParsec :: Parsec a => String -> Either ParseError a`
reactormonk 2017-02-22 08:12:18
There's all the parseFromFile stuff, but nothing without IO
ski 2017-02-22 08:12:33
mbrock : now, to *produce* a value of type `C a *> Foo a', you must produce evidence for `C a', and "bundle" it up (implicitly) with a value of type `Foo a'. to consume it, you may freely assume `C a' holds, and also use the value of type `Foo a'
reactormonk 2017-02-22 08:13:23
Ah, you simply use `parsec`. Blubb.
ski 2017-02-22 08:13:28
mbrock : we have a similar logical equivalence between `(C a *> Foo a) -> ...' and `C a => (Foo a -> ...)' ("currying" again)
ski 2017-02-22 08:14:09
mbrock : conceptually, a value of type `(C a *> Foo a)' is a pair of evidence for `C a' (e.g. a type class dictionary, with implementations of methods), coupled with a value of type `Foo a'
ski 2017-02-22 08:14:38
mbrock : while a value of type `C a => Foo a' conceptually is a function that when given evidence for `C a' will give you back a value of type `Foo a'
ski 2017-02-22 08:15:48
mbrock : again, `*>' is typically (but not always) coupled with an immediately preceding `exists'. like `[exists a. Show a *> Tree a]', perhaps
ski 2017-02-22 08:15:59
mbrock : is this making any sense ?
mbrock 2017-02-22 08:16:37
that last example seems to make sense
ski 2017-02-22 08:17:10
for each element of that list, there's some type `a', which is showable, such that the element is a tree with elements of type `a'
mbrock 2017-02-22 08:17:12
I see how that would let the consumer assume that (Show a) is true (because they would have access to the actual type class dictionary)
ski 2017-02-22 08:17:23
yes
ski 2017-02-22 08:18:10
if you moved the `exists' outside the list type constructor, then there'd be a single hidden/unknown/opaque/abstract type `a', for all the elements
ski 2017-02-22 08:18:45
with `exists' inside, it can be different for different elements (and so a consumer must treat the elements as if the `a' types actually *are* different, since they might be)
mbrock 2017-02-22 08:19:03
and `[forall a. Show a => Tree a]' would be the same kind of mostly useless type with only trivial/partial inhabitants as `[forall a. a]'
ski 2017-02-22 08:19:14
yep
ski 2017-02-22 08:19:38
using `Arbitary' instead of `Show', might be somewhat more useful, there
ski 2017-02-22 08:20:10
btw, you can easily do the `[exists a. Widget a *> a]' kind of OO thing here
ski 2017-02-22 08:20:33
existentials are related to OO, and to abstract data types. but these two uses use existentials in different ways
ski 2017-02-22 08:21:09
ADTs use existentials by making an existential record of operations (like the "queue" example above), opening it once, then using the operations inside directly
ski 2017-02-22 08:21:48
the "OO" version instead keeps repacking the current internal state (typed with the existentially quantified variable) with the operations/methods
ski 2017-02-22 08:22:34
with ADTs, it's easy to e.g. merge. not so with the OO approach here, since you only know the implementation of "yourself", not of other values that conform to the interface
ski 2017-02-22 08:22:49
.. but this is also an aside, unless you want to hear more about it
ski 2017-02-22 08:23:40
mbrock : what i wanted to get to was the two ways of encoding `exists' (and `*>') in GHC, so that you can actually use it
mbrock 2017-02-22 08:23:51
yeah
ski 2017-02-22 08:24:29
so, let's consider the type `exists q. (q,a -> q -> q,q -> Maybe (q,a)' again, the queue-ops example
ski 2017-02-22 08:24:59
so, the first encoding
ski 2017-02-22 08:25:09
it requires defining a new type (inventing a name)
ski 2017-02-22 08:25:35
so that instead of writing `exists q. (q,a -> q -> q,q -> Maybe (q,a))' in your type signature, you instead write `QueueOps a' (say)
ski 2017-02-22 08:26:13
(and it also requires wrapping and unwrapping of data constructor -- not that that is a big burden here, since usually one'd have to pack/unpack the triple here anyway)
ski 2017-02-22 08:26:23
so, we want to be able to say something like
ski 2017-02-22 08:26:39
data QueueOps a = MkQO (exists q. (q,a -> q -> q,q -> Maybe (q,a)))
threshold 2017-02-22 08:26:40
Sorry about earlier, I didn't mean to spam the lpaste link 3 times
ski 2017-02-22 08:27:55
mbrock : anyway, there's a different style of defining `data' types, that adds some extra power (though it's not strictly needed here). in this syntax, you instead explicitly specify the type signatures of the data constructors, like
ski 2017-02-22 08:28:02
data QueueOps a
ski 2017-02-22 08:28:06
where
ski 2017-02-22 08:28:23
MkQO :: (exists q. (q,a -> q -> q,q -> Maybe (q,a))) -> QueueOps a
ski 2017-02-22 08:28:28
mbrock : ok, so far ?
ski 2017-02-22 08:29:41
(btw, this style is called Generalized Algebraic Data Types, or GADTs (language extension) for short)
mbrock 2017-02-22 08:29:53
yep
ski 2017-02-22 08:32:00
if we want to consider `MkQO' as "just another operation, with a given type", the type signature (outside of the context of the `data' definition above) would be
ski 2017-02-22 08:32:02
MkQO :: forall a. (exists q. (q,a -> q -> q,q -> Maybe (q,a))) -> QueueOps a
ski 2017-02-22 08:32:02
(that's an aside)
mbrock 2017-02-22 08:32:02
I'm guessing we will make QueueOps into a type family thing? :)
ski 2017-02-22 08:32:02
nah :)
ski 2017-02-22 08:32:02
in any case, what you now should recall is the logical equivalence between `(exists a. ..a..) -> ...' and `forall a. (..a.. -> ...)', which means that we can now reformulate
ski 2017-02-22 08:32:02
MkQO :: (exists q. (q,a -> q -> q,q -> Maybe (q,a))) -> QueueOps a
ski 2017-02-22 08:32:02
as
ski 2017-02-22 08:32:03
MkQO :: forall q. (q,a -> q -> q,q -> Maybe (q,a)) -> QueueOps a
ski 2017-02-22 08:32:08
or, letting this `forall' also be implicit (since this is a type signature), just
ski 2017-02-22 08:32:15
MkQO :: (q,a -> q -> q,q -> Maybe (q,a)) -> QueueOps a
ski 2017-02-22 08:32:32
note that the data constructor `MkQO' is *polymorphic* in `q' (as well as `a')
ski 2017-02-22 08:33:00
it can work with any particular type `q' (and `a') the caller of `MkQO' decides to pick, when making a queue implementation
mbrock 2017-02-22 08:33:14
ah, ok, yes
ski 2017-02-22 08:33:21
e.g., perhaps `a' is picked as `Char', and `q' as `Text' (though that would probably not be so efficient for queues)
ski 2017-02-22 08:33:59
anyway, what's important here is that, while `a' is mentioned in the return type `QueueOps a' of the data constructor, the type variable `q' is *not* mentioned there !
ski 2017-02-22 08:34:28
this means that after picking `Char' for `a' and `Text' for `q', we get something of type `QueueOps Char', where there's now no trace any longer of `Text' being picked
ski 2017-02-22 08:35:15
iow, the choice of `Text' has been hidden from the result type. a consumer will have to treat `q' as abstract/opaque/unknown, since there's no way to recover it from the return type `QueueOps Char' (while `Char' *can* be recovered from that)
mbrock 2017-02-22 08:35:20
right, so when constructing a queue instance there needs to be an actual q, but it becomes abstract
ski 2017-02-22 08:35:33
*nod*, because it's elided from the return type
ski 2017-02-22 08:36:06
if one wants to use the GADT style, then any of the two last versions above suffices for defining `QueueOps'
ski 2017-02-22 08:36:20
if one wants to use the (older) non-GADT style, then one should type
ski 2017-02-22 08:36:39
data QueueOps a = forall a. MkQO (q,a -> q -> q,q -> Maybe (q,a))
ski 2017-02-22 08:36:49
er, sorry
ski 2017-02-22 08:36:52
data QueueOps a = forall q. MkQO (q,a -> q -> q,q -> Maybe (q,a))
ski 2017-02-22 08:37:39
the `forall' here means that the data constructor `MkQO' is *polymorphic* (in `q') .. which *effects/encodes* an existental quantification of the argument type, via the logical equivalence
ski 2017-02-22 08:37:46
people sometimes gets confused about this
ski 2017-02-22 08:37:51
if one would instead write
mbrock 2017-02-22 08:37:55
ok, and that's what's called an "existential type"? and it doesn't use an "exists" keyword because it's using this equivalence
ski 2017-02-22 08:38:00
data QueueOps a = MkQO (forall q. (q,a -> q -> q,q -> Maybe (q,a)))
ski 2017-02-22 08:38:41
then that would be *very* different, then `MkQO' would have a polymorphic *argument* (iow it would have a rank-two type), instead of *itself* being polymorphic (but forgetting `q' in the return type)
ski 2017-02-22 08:38:49
mbrock : right
ski 2017-02-22 08:39:13
also, you should note that the "existential" part really doesn't attach to the type itself, per se, but rather to the data *constructor*
ski 2017-02-22 08:39:30
you can easily have a type with some data constructors being "existential" in this way, while others are not
mbrock 2017-02-22 08:39:51
the data type definition is saying something like "for any q, you can construct a MkQO involving that q", but then to actually construct an MkQO you will use a concrete q
mbrock 2017-02-22 08:40:22
(or maybe you could somehow come up with a MkQO construction that works for any q)
ski 2017-02-22 08:40:32
but relatively often, when we use this feature, we only have one data constructor, often with only a single argument (i'll come to this), and so we use the term "existential data type" for the data type *encoding* the corresponding `exists q. ..q..'
ski 2017-02-22 08:40:57
mbrock : yes and yes (or for picking `q' as `Blah x' for any `x', say)
ski 2017-02-22 08:41:29
(or `x' is perhaps a type variable that you're being polymorphic in, and which also occurs in other places in your type signature of your operation)
ski 2017-02-22 08:42:10
anyway, instead of
ski 2017-02-22 08:42:14
data QueueOps a = forall a. MkQO (q,a -> q -> q,q -> Maybe (q,a))
ski 2017-02-22 08:42:21
we could choose to use
ski 2017-02-22 08:42:32
data QueueOps a = forall a. MkQO q (a -> q -> q) (q -> Maybe (q,a))
ski 2017-02-22 08:42:37
with multiple separate arguments
ski 2017-02-22 08:42:47
in GADT terms, this'd be
ski 2017-02-22 08:42:53
data QueueOpa a
ski 2017-02-22 08:42:54
where
ski 2017-02-22 08:43:18
MkQO :: forall q. q -> (a -> q -> q) -> (q -> Maybe (q,a)) -> QueueOps a
ski 2017-02-22 08:43:49
now, since this is of the form `forall q. (..q..) -> (..q..) -> (..q..) -> ...', we can't directly use the logical equivalence, short of uncurrying back again
ski 2017-02-22 08:44:08
still, we'd usually also call this an "existential data type"
ski 2017-02-22 08:44:15
one could also use record syntax, like
ski 2017-02-22 08:44:39
data QueueOps a = forall q. MkQO {emptyQ :: q,enqueue :: a -> q -> q,dequeue :: q -> Maybe (q,a)}
ski 2017-02-22 08:44:54
(it is also possible to specify record syntax, when using the GADT style)
