diff options
Diffstat (limited to 'events/src/Events/Spec/Types.hs')
-rw-r--r-- | events/src/Events/Spec/Types.hs | 11 |
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 | ||
14 | import Events.Types | 14 | import Events.Types |
15 | 15 | ||
16 | -- | A functional language reminiscent of typed lambda calculus with monadic | ||
17 | -- side-effects and foreign primitives | ||
16 | data Expr :: (* -> *) -> [*] -> * -> * where | 18 | data 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 | ||
41 | type family (xs :: [a]) ++ (ys :: [a]) :: [a] | 44 | type family (xs :: [a]) ++ (ys :: [a]) :: [a] where |
42 | type instance '[] ++ ys = ys | 45 | '[] ++ ys = ys |
43 | type instance (x ': xs) ++ ys = x ': (xs ++ ys) | 46 | (x ': xs) ++ ys = x ': (xs ++ ys) |
44 | infixr 5 ++ | 47 | infixr 5 ++ |
45 | 48 | ||