Hello there! I’d like to cautiously direct some attention to an article I wrote on working around the limitations of existential types in Haskell, with a technique I’ve dubbed “Existentials on a leash”.
It’s my first ever Haskell article, I haven’t found anyone to proofread it, and I’m doing unsafe things without formally proving that it’s really safe to do so, so please be gentle :).
The introduction reads as follows:
In this article, I will share a new workaround for the limited nature of existential quantification in current Haskell. Specifically, I will show the implementation of an Exists quantifier that relieves us from having to wrap existential type variables with a GADT constructor or with a higher-rank function (CPS-style), and instead allows them to appear “naked” in types. The quantifier is implemented as a type synonym for a function that linearly consumes a proof-token that ensures proper treatment of existentially typed values.
Additionally, I share an independent technique that ensures functions instantiate hidden (“non-naked”) existential types in their result with the same type as its input type is instantiated, i.e. they preserve the instantiation of hidden type variables. This technique also relies on linear types, but not the existential quantifier mentioned before. I will demonstrate this technique by implementing a safe variant of the unsafePartsOf:: Functor f => Traversing (->) f s t a b -> LensLike f s t [a] [b] optic combinator.
Both techniques use unsafeCoerce. I explain why I believe the coercions are safe, but I haven’t proven anything formally. Please try to break this stuff if you see some hole I have missed.
PS: I just realized the second part regarding the preservation of hidden type variables is actually not safe at all. A functor like Context allows Some values to escape their linear context. I’ll see if I can modify the code to make it safe within a reasonable amount of time and otherwise scrap it from the article. If anyone knows a way to unlist the post temporarily, that would be nice.
Hopefully fixed now. The CI job for a new Codespace prebuild will need ~1 hour to run.
I just skimmed this quickly and have two comments:
With a rank-2 type: (forall a. a -> r) -> r. This corresponds to exists a. (a -> r) -> r.
And it also corresponds simply to exists a. a.
If you implement dup as error "this is never used anyway" for a linearly captured function, you’d get away with it, and you could still write the conflict expression from before.
Would it be possible to make an unsatisfiable instance like this:
instance Unsatisfiable (Text "some informative error message")
=> Dupable (a %1 -> b) where ...
I just realized the second part regarding the preservation of hidden type variables is actually not safe at all. A functor like Context allows Some values to escape their linear context. I will amend the article shortly. Hopefully fixed now.
Frankly, I have no idea whether this is sound. It looks plausible though, kind of like destination-passing but for types (Fresh a operates like an empty reference to a type which gets filled exactly once).
Very clever at any rate.
The Ur/unur dance in order to prove the Dupable constraint in lazyVecFromList is rather unfortunate, I wonder if it could be improved. It would be nice, it would even go a long way to make this approach comfortable to use in many cases.
Indeed, there’s quite some friction where linear and non-linear code meet. Using the power of QuantifiedConstraints You can create an abstraction that covers quite a few cases though:
data UrSome f xs where
UrSome :: forall x f xs. f x :@@: xs %1 -> UrSome f xs
instance (forall x. Consumable (f x a)) => Consumable (UrSome f (LoT1 a)) where
consume (UrSome fa) = consume fa
instance (forall x. Dupable (f x a)) => Dupable (UrSome f (LoT1 a)) where
dupR (UrSome fa) = UrSome <$> dupR fa
wrapExists
:: forall f g a
. ( NL.Functor f
, (forall x. NL.Functor (g x))
, (forall x. Dupable (g x (Ur a)))
)
=> (forall x. f (Ur a) -> Exists x (g x (Ur a))) -> f a -> UrSome g (LoT1 a)
wrapExists f as =
unpack (UrSome @_ @g @(LoT1 (Ur a)) L.. f (NL.fmap Ur as))
& \(UrSome vec) -> UrSome $ NL.fmap (forget unur) vec
lazyVecFromList2 = wrapExists lazyVecFromList1
I’m still working my way through the article, but it seems like linearity is not necessary for the main idea of using Fresh as a witness of existential quantification?
Howdy, I haven’t yet read the whole article but in Current limitations of existential types you state:
With a rank-2 type: (forall a. a -> r) -> r.
This corresponds to exists a. (a -> r) -> r
(which is equivalent to exists a. a).
I believe your first & third may be equivalent (under assumptions) but the second one is not.
With the first one: (forall a. a -> r) -> r
If read with polymorphic r, then it connects to the third: forall r. (forall a. a -> r) -> r
Via curry/uncurry: forall r. ((exists a. a) -> r) -> r
Via yoneda: exists a. a
If read with a fixed r ~ R: (forall a. a -> R) -> R
Via curry/uncurry: ((exists a. a) -> R) -> R
Without knowing more about R you can’t get to exists a. a.
With the second one: exists a. (a -> r) -> r
I would read as either: forall r. (exists a. (a -> r) -> r) (exists a. (a -> R) -> R) (fixed r ~ R)
Neither of which connects to the first or third.
Now, if you happen to read that instead as: exists a. forall r. (a -> r) -> r
Then technically it is equivalent via yoneda,
but I think that would be an unusual reading,
and also not demonstrating anything about existentials.