I’m trying to write down a data type in PureScript for which I used GADTs in Idris. Roughly I had:
-- Idris data Task : Type -> Type where Edit : (val : Maybe a) -> Task a And : Show a => Show b => (left : Task a) -> (right : Task b) -> Task (Pair a b) ...
I need three things:
- Equate types to pin down the return type
- Introduce new existential types
- Save dictionaries for class instances
For (1) I could use
Type.Equality. I prefer the later, because I don’t have to fiddle with
symm, and friends. For (2) I could use
Data.Exists, but then I can’t access the existential type variable and use it for (1) and (3). How to specify I’d like to save a dictionary for
Show in that case?
I looked around and found this solution to use double negation to simulate existentials:
-- PureScript data Task r = Edit (Maybe r) | And (forall p. (forall a b. Show a => Show b => TypeEquals r (Tuple a b) => Task a -> Task b -> p) -> p) ...
I’ve three questions regarding this encoding.
First, when I try to create a
Show instance in the following way:
instance showTask :: Show a => Show (Task a) where ... show (And unpack) = unpack matcher where matcher x y = show x <> " <&> " <> show y
I get the error message
No type class instance was found for Data.Show.Show a1
When I make a hole to check the context:
show (And unpack) = unpack matcher where matcher x y = ?hole
The type variable b, bound at src/Data/Task/Minimal.purs line 24, column 30 - line 24, column 35 has escaped its scope (...)
What’s going on here?
Second, is this encoding trick still the way to go, or are there newer/better/more elegant solutions I could try?
And third, are there any plans to introduce language level support for existentials so we could write something like the code below and have support for it during pattern matching? Maybe it would be a stop-gap solution towards real GADTs, but useful nevertheless.
data Task r = Edit (Maybe r) | And (exist a b. Show a => Show b => TypeEquals r (Tuple a b) => Tuple (Task a) (Task b)) ...