Lambda calculus for computing events at runtime

1 files changed, 32 insertions, 0 deletions

diff --git a/events/src/Events/Spec/Types.hs b/events/src/Events/Spec/Types.hs
new file mode 100644
index 0000000..665958d
--- /dev/null
+++ b/events/src/Events/Spec/Types.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeOperators, KindSignatures, TypeFamilies, ExplicitNamespaces #-}
+
+module Events.Spec.Types
+  ( Expr(..)
+  , Val(..)
+  , Elem(..)
+  , Length(..)
+  , type (++)(..)
+  ) where
+
+data Expr :: (* -> *) -> [*] -> * -> * where
+  ELit :: Val m a -> Expr m ctx a
+  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
+
+type family Val m a where
+  Val m (a -> b) = Expr m '[a] b
+  Val m a        = m a
+
+data Elem :: a -> [a] -> * where
+  EZ :: Elem x (x ': xs)
+  ES :: Elem x xs -> Elem x (y ': xs)
+
+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)
+infixr 5 ++