Purescript GADT example

purescript-gadt.purs

module GADT.Main where

import Prelude (class Category, class Semigroupoid, (<<<), flip, identity, ($), (+), (==))

import Unsafe.Coerce (unsafeCoerce)

newtype Leibniz a b = Leibniz (forall f. f a -> f b)
infix 4 type Leibniz as ~

instance semigroupoidLeibniz :: Semigroupoid Leibniz where
  compose = flip trans
    where trans (Leibniz f) (Leibniz g) = Leibniz (g <<< f)

instance categoryLeibniz :: Category Leibniz where
  identity = Leibniz identity

coerce :: forall a b. a ~ b -> a -> b
coerce _ = unsafeCoerce


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


val :: Int -> Expr Int
val x = Val x identity

add :: Expr Int -> Expr Int -> Expr Int
add x y = Add x y identity

equal :: Expr Int -> Expr Int -> Expr Boolean
equal x y = Equal x y identity


eval :: forall a. Expr a -> a
eval (Val x p) = coerce p x
eval (Add x y p) = coerce p $ eval x + eval y
eval (Equal x y p) = coerce p $ eval x == eval y



main :: Boolean
main =
  let a = add (val 2) (val 5)
      b = add (val 1) (val 5)
      c = add (val 1) b
  in eval (equal a c)

hi