blob: 665958d9033f2a0a9297e4c581aee8a7d32f1993 (
plain)
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
|
{-# 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 ++
|
