Skip to content

Instantly share code, notes, and snippets.

@phadej
Last active October 12, 2016 13:18
Show Gist options
  • Save phadej/dc61b226be782782b670f4e0cc76bf11 to your computer and use it in GitHub Desktop.
Save phadej/dc61b226be782782b670f4e0cc76bf11 to your computer and use it in GitHub Desktop.
{-# LANGUAGE GADTs, TypeOperators, ScopedTypeVariables #-}
import Data.Eq.Type
data Expr e a where
Sum :: Expr x Int -> Expr [x] Int
-- | This is almost ADT, x is existential.
data Expr' e a where
Sum' :: [x] := e -> Int := a -> Expr' x a -> Expr' e a
fromExpr :: Expr e a -> Expr' e a
fromExpr (Sum e) = Sum' refl refl (fromExpr e)
toExpr :: forall e a. Expr' e a -> Expr e a
toExpr (Sum' proofE proofA e) = coerceBack $ Sum (coerceFwd $ toExpr e)
where
coerceBack = coerce (lift2' proofE proofA)
coerceFwd = coerce (lift2' refl (symm proofA))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment