GADT with tuples

LeibnizGADT.purs

module LeibnizGADT where

import Prelude

import Control.Monad.Eff.Exception.Unsafe (unsafeThrow)
import Data.Leibniz (type (~), coerce, coerceSymm, liftLeibniz, liftLeibniz1of2, liftLeibniz2of2, lowerLeibniz1of2, lowerLeibniz2of2, symm)
import Data.Tuple (Tuple(..))

-- Solution to https://www.reddit.com/r/purescript/comments/4x1jq3/approximating_gadts_in_purescript/d6bzlez/
data T a
  = B Boolean (Boolean ~ a)
  | I Int (Int ~ a)
  -- quasi-Day encoding of an existential tuple thingy via continuations
  | P (forall r. (forall x y. (Tuple x y ~ a) -> T x -> T y -> r) -> r)

eval :: forall a. T a -> a
eval (B b p) = coerce p b
eval (I i p) = coerce p i
eval (P e) = e \p l r -> coerce p (Tuple (eval l) (eval r))

addT :: forall a. Partial => T a -> T a -> T a
addT (B b1 p1) (B b2 p2) = B (b1 || b2) p1
addT (I i1 p1) (I i2 p2) = I (i1 + i2) p1
addT (P e1) (P e2) =
  let
    i :: forall x1 y1 x2 y2.
      (Tuple x1 y1 ~ a) -> T x1 -> T y1 ->
      (Tuple x2 y2 ~ a) -> T x2 -> T y2 ->
      T a
    i = \p1 l1 r1 -> \p2 l2 r2 ->
      let
        -- we know a ~ a so we can get that the tuples are equal
        comp :: Tuple x1 y1 ~ Tuple x2 y2
        comp = p1 >>> symm p2
        -- and their components
        left :: x1 ~ x2
        left = lowerLeibniz1of2 comp
        right :: y1 ~ y2
        right = lowerLeibniz2of2 comp
        -- and constructions with their components
        leftT :: T x1 ~ T x2
        leftT = liftLeibniz left
        rightT :: T y1 ~ T y2
        rightT = liftLeibniz right
        -- so convert these over to the "other" (same) type
        l2' :: T x1
        l2' = coerceSymm leftT l2
        r1' :: T y2
        r1' = coerce rightT r1
        -- note that I select x1 for the left addition and y2 for the right
        -- but this proves it doesn't matter:
        p1' :: Tuple x1 y2 ~ a
        p1' = liftLeibniz2of2 (symm right) >>> p1
        p2' :: Tuple x1 y2 ~ a
        p2' = liftLeibniz1of2 left >>> p2
      in P \e -> e p1' (addT l1 l2' :: T x1) (addT r1' r2 :: T y2)
  in e1 (e2 i)
addT (I _ p1) (B _ p2) = contraIB p1 p2
addT (B _ p1) (I _ p2) = contraIB p2 p1

-- urgh, disequality proofs are the worst
-- need instance chainz
contraIB :: forall a b. (Int ~ a) -> (Boolean ~ a) -> b
contraIB _ _ = unsafeThrow "Contradicting proofs"