Getting existential - Haskell

@rae (Simplifying Constraint Solving in GHC):

I'm hoping, in the next 6 months or something, to have a new extension for GHC that just makes existential types work as easily as universal types...

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 like

IsList (exists n. Vec n a)

or

toSing :: exists x. SingKind a => a -> Sing (x :: a)

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.

bradrn said:

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

data Some where
  Some :: forall a. 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:

case x :: Some of Some a -> _

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:

data Any where
  Any :: (forall a. a) -> Any

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

TheMatten said:

bradrn said:

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

(It doesn't matter whether they're wrapped in another datatype or CPS function)

TheMatten said:

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.)

:100:
I've seen Some defined here and there, but it seems like people usually define it themselves, maybe to avoid dependencies

TheMatten said:

:100:
I've seen Some defined here and there, but it seems like people usually define it themselves, maybe to avoid dependencies

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:

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

from the reflex-frp ecosystem

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:

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.

Alex Chapman said:

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.)

bradrn 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.)

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

Alex Chapman said:

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 :: forall a. exists n. [a] -> Vec n a

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

Vec n a -> Vec n a

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

data SomeVec a where
  SomeVec :: forall n. Vec n a -> SomeVec a

withVec :: forall a r. SomeVec a -> (forall n. Vec n a -> r) -> r
withVec (SomeVec v) f = f v

toList :: forall a. [a] -> SomeVec a

> withVec sv \v -> ...

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.html

I 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