summaryrefslogtreecommitdiff
path: root/events/src/Events/Spec/Types.hs
diff options
context:
space:
mode:
Diffstat (limited to 'events/src/Events/Spec/Types.hs')
-rw-r--r--events/src/Events/Spec/Types.hs11
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
13 13
14import Events.Types 14import Events.Types
15 15
16-- | A functional language reminiscent of typed lambda calculus with monadic
17-- side-effects and foreign primitives
16data Expr :: (* -> *) -> [*] -> * -> * where 18data Expr :: (* -> *) -> [*] -> * -> * where
17 ELit :: Val m a -> Expr m ctx a 19 EVal :: Val m a -> Expr m ctx a
20 EPri :: (Val m a -> Expr m ctx b) -> Expr m (a ': ctx) b
18 EVar :: Elem a ctx -> Expr m ctx a 21 EVar :: Elem a ctx -> Expr m ctx a
19 ELam :: Expr m (arg ': ctx) res -> Expr m ctx (arg -> res) 22 ELam :: Expr m (arg ': ctx) res -> Expr m ctx (arg -> res)
20 EApp :: Expr m ctx (arg -> a) -> Expr m ctx arg -> Expr m ctx a 23 EApp :: Expr m ctx (arg -> a) -> Expr m ctx arg -> Expr m ctx a
@@ -38,8 +41,8 @@ data Length :: [a] -> * where
38 LZ :: Length '[] 41 LZ :: Length '[]
39 LS :: Length xs -> Length (x ': xs) 42 LS :: Length xs -> Length (x ': xs)
40 43
41type family (xs :: [a]) ++ (ys :: [a]) :: [a] 44type family (xs :: [a]) ++ (ys :: [a]) :: [a] where
42type instance '[] ++ ys = ys 45 '[] ++ ys = ys
43type instance (x ': xs) ++ ys = x ': (xs ++ ys) 46 (x ': xs) ++ ys = x ': (xs ++ ys)
44infixr 5 ++ 47infixr 5 ++
45 48