ConstMemDlc.hs

{-# 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 ""