Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
{-# LANGUAGE GADTs, TypeOperators, DeriveFunctor, DataKinds, KindSignatures, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, OverlappingInstances, TypeFamilies, UndecidableInstances, FunctionalDependencies, ScopedTypeVariables #-}
module ConstMemDlc where
import qualified Data.Map as Map
import Data.Proxy
import GHC.TypeLits
import Data.Type.Equality
data Lit a = Lit Int
data Add a = Add a a deriving (Functor, Eq)
data Mult a = Mult a a deriving Functor
----------------------------------
type family Idx (n :: Nat) (fs :: [* -> *]) :: (* -> *) where
Idx 0 (f ': fs) = f
Idx n (f ': fs) = Idx (n-1) fs
type family Find (f :: * -> *) (fs :: [* -> *]) :: Nat where
Find f (f ': fs) = 0
Find f (g ': fs) = 1 + (Find f fs)
data Sum (fs :: [* -> *]) a where
InSum :: Elem f fs -> f a -> Sum fs a
data Elem f fs where
Elem :: (KnownNat n, Idx n fs ~ f) => Proxy n -> Elem f fs
class (Idx (Find f fs) fs ~ f, KnownNat (Find f fs)) => Mem f fs where
witness :: Elem f fs
instance (Idx n fs ~ f, Find f fs ~ n, KnownNat n) => Mem f fs where
witness = Elem (Proxy :: Proxy (Find f fs))
prj :: Elem f fs -> Sum fs a -> Maybe (f a)
prj (Elem a) (InSum (Elem b) x) = case sameNat a b of
Just Refl -> Just x
Nothing -> Nothing
type Sig = Sum '[Lit, Add, Mult]
data Term f = Term (f (Term f))
inject :: Mem f fs => f (Term (Sum fs)) -> Term (Sum fs)
inject x = Term (InSum witness x)
lit :: Int -> Term Sig
lit n = inject $ Lit n
add :: Term Sig -> Term Sig -> Term Sig
add x y = inject $ Add x y
expr1 = add (lit 42) (add (lit 1) (lit 2))
main = putStrLn ""
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment