I don't understand what that's about. I only recently learned that forall just declares type variables, and doesn't require inscrutable mathematical knowledge. Is there a similar programmer-language explanation of exists?

I’m not quite sure what you’re talking about… Haskell doesn’t have an exists keyword. (Unless you’re talking about existential types, but those use forall as well.)

I'm talking about one of the GHC developers being interested in improving support for existential types in GHC - and what I'm saying is that if that means real existential quantifier, then it would unlock new abilities and remove wrappers in some existing code.

@Alex Chapman Nothing advanced really, it's just difference in who get's to pick the concrete type in place of the variable - when you say x :: forall a. Maybe a, you say that given x will work for whatever a you choose as a user - so you could use it as Maybe Int or Maybe String etc. (BTW, that would mean that x = Nothing)
With x :: exists a. Maybe a for some hypothetical exists quantifier, you say that x uses some concrete type in place of a which you don't know about, is opaque to you - so compared to first example, such x could be e.g. Just 'x' or Just [1,2,3] or whatever else, and it's user wouldn't be allowed to see what the concrete a is without more information.

I’m not quite sure what you’re talking about… Haskell doesn’t have an exists keyword. (Unless you’re talking about existential types, but those use forall as well.)

The only use forall in a sense of being encoded by forall used in right way - e.g. with

dataSomewhereSome::foralla.a->Some

when you treat constructor Some as a function, then the a is just an ordinary universally quantified variable - what matters is that in case of constructors, we can actually deconstruct them using patterns:

casex::SomeofSomea->_

And when you do that, given that you were able to put anything into Some because of it's polymorphic type, what's the type of a? Well, it's something already picked which we don't get to choose - that is, existential variable. Compare this to:

dataAnywhereAny::(foralla.a)->Any

where Any can only be supplied with undefined, but it's field can be used as any type once pattern-matched on.

I’m not quite sure what you’re talking about… Haskell doesn’t have an exists keyword. (Unless you’re talking about existential types, but those use forall as well.)

The only use forall in a sense of being encoded by forall used in right way …

Yes, I do understand this (I’ve made heavy use of existential types myself); I was merely commenting on the syntax, that ‘existential types’ are still defined with forall.

Oh, I see - I've mentioned exists under If - I'm not sure if that's what the quote actually implies, but I can't think of any other conclusion - the single big pain point of existentials in Haskell is that they always have to be wrapped, even though normal datypes in Haskell are boxed anyway

the single big pain point of existentials in Haskell is that they always have to be wrapped

Oh, yes. Existential types are useful, but this makes them such a pain to work with. It’s particularly bad with existentially-quantified records, since record construction and field access doesn’t work properly under existentials. I end up having to create a special boxing type for the records, so I can unwrap it to modify the record and then re-wrap it to hide the type variable. (I have wondered on occasion why no-one seems to have defined a type data Some t = Some (forall a. t a) to make the boxing/unboxing a bit easier.)

Thanks for the explanation, @TheMatten. So would it be right to say that with this hypothetical exists keyword, the implementer would choose the type to instantiate the type variable with, in contrast with forall, in which the caller chooses the type?

But if the implementer wants to hide the type from the caller, why expose it in the type signature?

This is exactly correct. If the implementer wants to hide the type from the caller, they can define a type like ThisHasAHiddenTypeVariable = Hide (forall a. Maybe a); they can then use the type ThisHasAHiddenTypeVariable without exposing the variable a in the type signature.

So would it be right to say that with this hypothetical exists keyword, the implementer would choose the type to instantiate the type variable with, in contrast with forall, in which the caller chooses the type?

Almost, but not quite. You can get situations when using forall in which the implementer is the one to choose the type, e.g. in type signatures like thisHasAHiddenTypeVariable :: (forall a. Maybe a -> b) -> b. (Note that this type is in fact isomorphic to the ThisHasAHiddenTypeVarible type which I defined above.)

Almost, but not quite. You can get situations when using forall in which the implementer is the one to choose the type, e.g. in type signatures like thisHasAHiddenTypeVariable :: (forall a. Maybe a -> b) -> b. (Note that this type is in fact isomorphic to the ThisHasAHiddenTypeVarible type which I defined above.)

Actually, I would say that @Alex Chapman's description still applies, it's just put on it's head because of RankNTypes - when you think about it, thisHasAHiddenTypeVariable chooses the type in place of a because it's actually the caller - it may take the function as an argument, but it still calls it in same way as any other polymorphic function, while the caller of thisHasAHiddenTypeVariable is actually the implementer of the provided continuation

But if the implementer wants to hide the type from the caller, why expose it in the type signature?

Because often you don't really want to hide it, you just "can't expose it" - this is often the case with dynamically constructed GADTs
E.g. in case of

fromList::foralla.existsn.[a]->Vecna

you may want to immediately pass such value some other function, e.g. with signature

Vecna->Vecna

Compared to

[a]->[a]

such type is actually more precise because it forces length of the vector to stay the same. For that, you don't need to know the precise length of the vector, but you need to be able to talk about it to say that you want to preserve it. Compare this to current approach of doing

@rae (Simplifying Constraint Solving in GHC):

People, if I understand it right, this is going to change programming with GADTs A LOT

If we get

`exists`

quantifier, we may be able to do stuff likeor

I don't understand what that's about. I only recently learned that

`forall`

just declares type variables, and doesn't require inscrutable mathematical knowledge. Is there a similar programmer-language explanation of`exists`

?I’m not quite sure what you’re talking about… Haskell doesn’t have an

`exists`

keyword. (Unless you’re talking about existentialtypes, but those use`forall`

as well.)I'm talking about one of the GHC developers being interested in improving support for existential types in GHC - and what I'm saying is that if that means real existential quantifier, then it would unlock new abilities and remove wrappers in some existing code.

@Alex Chapman Nothing advanced really, it's just difference in who get's to pick the concrete type in place of the variable - when you say

`x :: forall a. Maybe a`

, you say that given`x`

will work for whatever`a`

you choose as a user - so you could use it as`Maybe Int`

or`Maybe String`

etc. (BTW, that would mean that`x = Nothing`

)With

`x :: exists a. Maybe a`

for some hypothetical`exists`

quantifier, you say that`x`

uses some concrete type in place of`a`

which you don't know about, is opaque to you - so compared to first example, such`x`

could be e.g.`Just 'x'`

or`Just [1,2,3]`

or whatever else, and it's user wouldn't be allowed to see what the concrete`a`

is without more information.bradrn said:

The only use

`forall`

in a sense of being encoded by`forall`

used in right way - e.g. withwhen you treat constructor

`Some`

as a function, then the`a`

is just an ordinary universally quantified variable - what matters is that in case of constructors, we can actually deconstruct them using patterns:And when you do that, given that you were able to put anything into

`Some`

because of it's polymorphic type, what's the type of`a`

? Well, it'ssomethingalready picked which we don't get to choose - that is, existential variable. Compare this to:where

`Any`

can only be supplied with`undefined`

, but it's field can be used as any type once pattern-matched on.TheMatten said:

Yes, I do understand this (I’ve made heavy use of existential types myself); I was merely commenting on the syntax, that ‘existential types’ are still defined with

`forall`

.Oh, I see - I've mentioned

`exists`

underIf- I'm not sure if that's what the quote actually implies, but I can't think of any other conclusion - the single big pain point of existentials in Haskell is that they always have to be wrapped, even though normal datypes in Haskell are boxed anyway(It doesn't matter whether they're wrapped in another datatype or CPS function)

TheMatten said:

Oh, yes. Existential types are useful, but this makes them

sucha pain to work with. It’s particularly bad with existentially-quantified records, since record construction and field access doesn’t work properly under existentials. I end up having to create a special boxing type for the records, so I can unwrap it to modify the record and then re-wrap it to hide the type variable. (I have wondered on occasion why no-one seems to have defined a type`data Some t = Some (forall a. t a)`

to make the boxing/unboxing a bit easier.):100:

I've seen

`Some`

defined here and there, but it seems like people usually define it themselves, maybe to avoid dependenciesTheMatten said:

OK, I hadn’t known this… perhaps I’ll do the same next time I need to work with existentials.

https://hackage.haskell.org/package/some

from the reflex-frp ecosystem

Torsten Schmits said:

Thanks for this, I didn’t know this package existed! I’ll probably end up using this one in my next project.

Thanks for the explanation, @TheMatten. So would it be right to say that with this hypothetical

`exists`

keyword, the implementer would choose the type to instantiate the type variable with, in contrast with`forall`

, in which the caller chooses the type?But if the implementer wants to hide the type from the caller, why expose it in the type signature?

Alex Chapman said:

This is exactly correct. If the implementer wants to hide the type from the caller, they can define a type like

`ThisHasAHiddenTypeVariable = Hide (forall a. Maybe a)`

; they can then use the type`ThisHasAHiddenTypeVariable`

without exposing the variable`a`

in the type signature.Alex Chapman said:

Almost, but not quite. You can get situations when using

`forall`

in which the implementer is the one to choose the type, e.g. in type signatures like`thisHasAHiddenTypeVariable :: (forall a. Maybe a -> b) -> b`

. (Note that this type is in fact isomorphic to the`ThisHasAHiddenTypeVarible`

type which I defined above.)bradrn said:

Actually, I would say that @Alex Chapman's description still applies, it's just put on it's head because of

`RankNTypes`

- when you think about it,`thisHasAHiddenTypeVariable`

chooses the type in place of`a`

because it's actually the caller - it may take the function as an argument, but it still calls it in same way as any other polymorphic function, while the caller of`thisHasAHiddenTypeVariable`

is actually the implementer of the provided continuationAlex Chapman said:

Because often you don't really want to hide it, you just "can't expose it" - this is often the case with dynamically constructed

`GADTs`

E.g. in case of

you may want to immediately pass such value some other function, e.g. with signature

Compared to

such type is actually more precise because it forces length of the vector to stay the same. For that, you don't need to know the precise length of the vector, but you need to be able to talk about it to say that you want to preserve it. Compare this to current approach of doing

BTW, totally irrelevant in practice, but if someone wonders why you can encode these quantifiers in terms of each other, it's because they're adjoint

I wouldn't say totally irrelevant - isn't there some systematic way to get the adjoint of something?

so then, if someone doesn't know how to do the encoding, they could consult the systematic way

should be possible, but I'd assume it's harder to get you head around than the haskell part :sweat_smile:

@Georgi Lyubenov // googleson78 there's is, but in Haskell the existing implementation is limited to

`Hask`

endofunctors: https://hackage.haskell.org/package/adjunctions-4.4/docs/Data-Functor-Adjunction.htmlI assumed @Georgi Lyubenov // googleson78 meant to derive the equation in your head with galois connections

no clue what galois connections mean in CT but yeah

just a generalization of adjunctions to posets, I think

Ah, I see