Initial work on builtin constants

1 files changed, 7 insertions, 4 deletions

diff --git a/events/src/Events/Spec/Types.hs b/events/src/Events/Spec/Types.hs
index 5216f46..c7fd058 100644
--- a/events/src/Events/Spec/Types.hs
+++ b/events/src/Events/Spec/Types.hs
@@ -13,8 +13,11 @@ module Events.Spec.Types
 
 import Events.Types
 
+-- | A functional language reminiscent of typed lambda calculus with monadic
+-- side-effects and foreign primitives
 data Expr :: (* -> *) -> [*] -> * -> * where
-  ELit :: Val m a -> Expr m ctx a
+  EVal :: Val m a -> Expr m ctx a
+  EPri :: (Val m a -> Expr m ctx b) -> Expr m (a ': ctx) b
   EVar :: Elem a ctx -> Expr m ctx a
   ELam :: Expr m (arg ': ctx) res -> Expr m ctx (arg -> res)
   EApp :: Expr m ctx (arg -> a) -> Expr m ctx arg -> Expr m ctx a
@@ -38,8 +41,8 @@ data Length :: [a] -> * where
   LZ :: Length '[]
   LS :: Length xs -> Length (x ': xs)
 
-type family (xs :: [a]) ++ (ys :: [a]) :: [a]
-type instance '[]       ++ ys = ys
-type instance (x ': xs) ++ ys = x ': (xs ++ ys)
+type family (xs :: [a]) ++ (ys :: [a]) :: [a] where
+  '[]       ++ ys = ys
+  (x ': xs) ++ ys = x ': (xs ++ ys)
 infixr 5 ++