Understanding TypeEquals

Help
#1

How would we convert this:

import Data.Leibniz (type (~))

data Expr a
  = Add (Expr Int) (Expr Int) (a ~ Int)
  | Eq (Expr Int) (Expr Int) (a ~ Boolean)
  | Not (Expr Boolean) (a ~ Boolean)
  | Val Int (a ~ Int)

to using Type.Equality? The goal would be to approximate GADTs such as explained here https://hgiasac.github.io/posts/2018-12-18-PureScript-GADTs-Alternatives---Recap.html (which uses Leibniz).

To get something like eval :: forall a. Expr a -> a that works. Is this even possible? I’m trying to wrap my head around this and tried a bunch of things none of which worked. This doesn’t seem to be a great idea:

data Expr a
  = Add (TypeEquality a Int => Expr a) (TypeEquality a Int => Expr a)
  | Eq (TypeEquality a Boolean => Expr a) (TypeEquality a Boolean => Expr a)
  | Not (TypeEquality a Boolean => Expr a)
  | Val (TypeEquality a Int => a)

And other similar forma all fail. Thanks :slight_smile:

#2

I believe this works? Been a while since I’ve done this stuff, mostly got there by putting stuff together:

import Prelude ((==))
import Type.Equality (class TypeEquals, to)

data Expr a
  = Val Int (forall r. (TypeEquals Int a => Int -> r) -> Int -> r)
  | Eq (Expr Int) (Expr Int) (forall r. (TypeEquals Boolean a => Boolean -> r) -> Boolean -> r)

-- Note that \f x -> f x is NOT the same as apply, as it captures the constraint dictionary
eq' :: forall a. TypeEquals Boolean a => Expr Int -> Expr Int -> Expr a
eq' l r = Eq l r (\f x -> f x)

val :: forall a. TypeEquals Int a => Int -> Expr a
val v = Val v (\f x -> f x)

-- valWrong :: Int -> Expr Int
-- valWrong v = Val v (\_ _ -> 0)

eval :: forall a. Expr a -> a
eval (Val v proof) = proof to v
eval (Eq l r proof) = proof to ((eval l) == (eval r))

The general idea is that the only valid implementation of the final argument for each constructor are the ones used in eq' and val, and the only way to get an a from an Expr a is the way it’s done in eval

2 Likes
#3

Realised I didn’t need the constraint on the smart constructors (as they solve the instance search inside), and you can also add an alias to make it appear like leibniz:

import Prelude ((==))
import Type.Equality (class TypeEquals, to)

type TE b a = forall r. (TypeEquals a b => a -> r) -> a -> r
infix 4 type TE as ~

data Expr a
  = Val Int (a ~ Int)
  | Eq (Expr Int) (Expr Int) (a ~ Boolean)

-- Note that \f x -> f x is NOT the same as apply, as it captures the constraint
-- dictionary for which the instance must be found here
eq' :: Expr Int -> Expr Int -> Expr Boolean
eq' l r = Eq l r (\f x -> f x)

val :: Int -> Expr Int
val v = Val v (\f x -> f x)

-- valWrong :: Int -> Expr Int
-- valWrong v = Val v (\_ _ -> 0)

eval :: forall a. Expr a -> a
eval (Val v proof) = proof to v
eval (Eq l r proof) = proof to ((eval l) == (eval r))
1 Like
#4

Ah, I have realised it doesn’t quite work, as you can still ‘attack’ by modifying/ignoring the x:

valBad :: Int -> Expr Int
valBad v = Val v (\f _ -> f 0)

And just realised the fix:

type TE b a = forall ra rb. (TypeEquals a b => ra -> rb) -> ra -> rb
infix 4 type TE as ~
...
#5

Thanks a lot. This goes way beyond my comprehension right now, but I’m glad someone went through it “on paper” cause I couldn’t find any references anywhere about using TypeEquals for simulating GADTs so it’s much appreciated.

Do you know any resources where some of this stuff is explained to get some understanding of what’s happening with this code?

Thanks again :slight_smile:

1 Like
#6

https://thimoteus.github.io/posts/2018-09-21-existential-types.html made me more comfortable using constraints in the ‘rank-2’ position, although there they are being used for a different reason

I also found that looking at the compiled output of code helped me understand where/when type class constraint instances were being solved and passed around, as part of the key to the previous code is forcing the instance of TypeEquals to always be found to be able implement the TE function (thus enabling us to guarantee the a in Expr is always what we wanted, as TypeEquals will fail if it is anything else)

I can’t really remember what other resources I looked at unfortunately as it’s been a while

2 Likes
#7

I can’t explain it deeply right now, but there’s an important difference between the following two types which if you can grasp will help you understand the GADT approximation:

newtype One a = One (Show a => a -> String)
newtype Two a = Two ((Show a => a -> String) -> a -> String)

The key really is that the function inside One only searches for the Show instance when it’s called, whereas Two searches for the Show instance when Two is constructed.

That, in combination with the right use of forall, makes it so the implementer doesn’t know enough about the types to do anything other than the correct implementation (in the same way that forall a. a -> a only has one possible implementation)

2 Likes
#8

I have to say, that link about existential types didn’t help as much, I at least didn’t think it’s a good explanation and there’s some typos in too.

But combined with these:

It’s starting to make more sense.

3 Likes