1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
{-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeOperators, KindSignatures, TypeFamilies, ExplicitNamespaces #-}
{-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
module Events.Spec.Types
( Expr(..)
, Val(..)
, Bindable(..)
, Spec
, Elem(..)
, Length(..)
, type (++)(..)
, module Events.Types
) where
import Events.Types
-- | A functional language reminiscent of typed lambda calculus with monadic
-- side-effects and foreign primitives
data Expr :: (* -> *) -> [*] -> * -> * where
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
type family Val m a where
Val m (a -> b) = Expr m '[a] b
Val m a = m a
type family Ctx m f where
Ctx m (m a -> b) = (a ': Ctx m b)
Ctx m a = '[]
type family Fin m f where
Fin m (m a -> b) = Fin m b
Fin m (m a) = a
Fin m a = a
class Bindable m a where
liftE :: a -> Expr m (Ctx m a) (Fin m a)
instance (Val m a ~ m a, Bindable m b) => Bindable m (m a -> b) where
liftE :: (m a -> b) -> Expr m (a ': Ctx m b) (Fin m b)
liftE = (EPri :: (Val m a -> Expr m (Ctx m b) (Fin m b)) -> Expr m (a ': Ctx m b) (Fin m b)) . ((liftE :: b -> Expr m (Ctx m b) (Fin m b)) . )
instance {-# OVERLAPPABLE #-} (Val m a ~ m a, Val m b ~ m b, Ctx m (m b) ~ '[], Fin m (m b) ~ b) => Bindable m (m a -> m b) where
liftE :: (m a -> m b) -> Expr m '[a] b
liftE = EPri . (EVal .)
instance (Val m a ~ m a, Fin m (m a) ~ a, Ctx m (m a) ~ '[]) => Bindable m (m a) where
liftE :: m a -> Expr m '[] a
liftE = EVal
type Spec m = Expr (Eval m) '[] ()
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] where
'[] ++ ys = ys
(x ': xs) ++ ys = x ': (xs ++ ys)
infixr 5 ++
|