Encoding GADT like data type

Help
#1

Hi all!

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:

  1. Equate types to pin down the return type
  2. Introduce new existential types
  3. Save dictionaries for class instances

For (1) I could use Data.Leibniz or Type.Equality. I prefer the later, because I don’t have to fiddle with coerce, 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

I get:

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

Unfortunately, there are no top-secret language tools to make this easier :smiley:

As far as the missing constraint and type error, you will definitely need to add a type signature to matcher, or just use a lambda inline. PureScript does not let-generalize, and it won’t infer the appropriate polymorphic signature required by unpack.

Note that you still must use coercion functions with TypeEquality. The compiler does not implicitly look for equality constraints, so you’ll have to judicially use to and from to go back and forth just as you would with Leibniz.

1 Like
#3

You could try using a final tagless encoding:

class IsTask rep where
  edit :: Maybe a -> rep a
  end :: forall a b. Show a => Show b => rep a -> rep b -> rep (Pair a b)
  ...

type Task a  = forall rep. IsTask rep => rep a
5 Likes
#4

Thanks Nathan, the lambda helps indeed :wink: Didn’t think about difficulties with type inference using universal types :see_no_evil:.

I’ll probably run into TypeEquality.to and from after implementing more.

#5

Looks interesting Phil, I’ll try it out and see which one is better for my use case.

Thank you both for the really quick response!