Lambda calculus for computing events at runtime

3 files changed, 99 insertions, 0 deletions

diff --git a/events/src/Events/Spec/Eval.hs b/events/src/Events/Spec/Eval.hs
new file mode 100644
index 0000000..3a23e0b
--- /dev/null
+++ b/events/src/Events/Spec/Eval.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE GADTs, DataKinds, TypeOperators, RankNTypes, ScopedTypeVariables #-}
+
+module Events.Spec.Eval
+  ( evalExpr
+  ) where
+
+import Events.Spec.Types
+
+shift :: forall m ts2 t x. Expr m ts2 x -> Expr m (t ': ts2) x
+shift = shift' LZ
+  where
+    -- shift' :: forall ts1 ts2 t x. Length ts1 -> Expr (ts1 ++ ts2) x -> Expr (ts1 ++ t ': ts2) x
+    shift' :: forall ts1 x. Length ts1 -> Expr m (ts1 ++ ts2) x -> Expr m (ts1 ++ t ': ts2) x
+    shift' _ (ELit x)   = ELit x
+    shift' l (EVar v)   = EVar $ shiftElem l v
+    shift' l (ELam b)   = ELam $ shift' (LS l) b
+    shift' l (EApp f x) = EApp (shift' l f) (shift' l x)
+  
+    shiftElem :: forall ts1 u. Length ts1 -> Elem u (ts1 ++ ts2) -> Elem u (ts1 ++ t ': ts2)
+    shiftElem LZ e = ES e
+    shiftElem (LS _) EZ = EZ
+    shiftElem (LS l) (ES e) = ES $ shiftElem l e
+    
+
+beta = flip beta' LZ
+beta' :: forall m ts1 ts2 s t. Expr m ts2 s -> Length ts1 -> Expr m (ts1 ++ s ': ts2) t -> Expr m (ts1 ++ ts2) t
+beta' _  _     (ELit x)      = ELit x
+beta' e  LZ    (EVar  EZ   ) = e
+beta' _  LZ    (EVar (ES v)) = EVar v
+beta' _ (LS _) (EVar  EZ   ) = EVar EZ
+beta' e (LS l) (EVar (ES v)) = shift $ beta' e l (EVar v)
+beta' e  l     (ELam b)      = ELam $ beta' e (LS l) b
+beta' e  l     (EApp f a)    = EApp (beta' e l f) (beta' e l a)
+
+evalExpr :: Expr m '[] t -> Val m t
+evalExpr (ELit a)   = a
+evalExpr (ELam a)   = a
+evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f)
diff --git a/events/src/Events/Spec/LICENSE b/events/src/Events/Spec/LICENSE
new file mode 100644
index 0000000..c28fee7
--- /dev/null
+++ b/events/src/Events/Spec/LICENSE
@@ -0,0 +1,29 @@
+The code in siblings of this file is either heavily inspired by or copied from [glambda](https://hackage.haskell.org/package/glamba), an interpreter for a simply typed lambda-calculus by Richard Eisenberg under the following license:
+
+Copyright (c) 2015, Richard Eisenberg
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+this list of conditions and the following disclaimer in the documentation
+and/or other materials provided with the distribution.
+
+3. Neither the name of the author nor the names of its contributors may be
+used to endorse or promote products derived from this software without
+specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
\ No newline at end of file
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 ++