blob: 37a766ecef553cd01d0dfef03ad7d8816d827fa0 (
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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
{-# LANGUAGE ScopedTypeVariables, TypeOperators, DataKinds, PolyKinds,
TypeFamilies, GADTs, StandaloneDeriving, StandaloneKindSignatures #-}
module SplitWD where
import Data.Kind ( Type )
data Nat = Zero | Succ Nat
type family a + b where
Zero + b = b
Succ a + b = Succ (a + b)
infixl 6 +
data Vec :: Type -> Nat -> Type where
VNil :: Vec a Zero
(:>) :: a -> Vec a n -> Vec a (Succ n)
infixr 5 :>
type (+++) :: Vec a n -> Vec a m -> Vec a (n + m)
type family xs +++ ys where
VNil +++ ys = ys
(x :> xs) +++ ys = x :> (xs +++ ys)
infixr 5 +++
data Exp :: Vec Type n -> Type -> Type where
Var :: Elem xs x -> Exp xs x
data Elem :: forall a n. Vec a n -> a -> Type where
Here :: Elem (x :> xs) x
There :: Elem xs x -> Elem (y :> xs) x
-- | @Length xs@ is a runtime witness for how long a vector @xs@ is.
-- @LZ :: Length xs@ says that @xs@ is empty.
-- @LS len :: Length xs@ tells you that @xs@ has one more element
-- than @len@ says.
-- A term of type @Length xs@ also serves as a proxy for @xs@.
data Length :: forall a n. Vec a n -> Type where
LZ :: Length VNil
LS :: Length xs -> Length (x :> xs)
deriving instance Show (Length xs)
-- | Convert an expression typed in one context to one typed in a larger
-- context. Operationally, this amounts to de Bruijn index shifting.
-- As a proposition, this is the weakening lemma.
shift :: forall ts2 t ty. Exp ts2 ty -> Exp (t :> ts2) ty
shift = go LZ
where
go :: forall ts1 ty. Length ts1 -> Exp (ts1 +++ ts2) ty -> Exp (ts1 +++ t :> ts2) ty
go l_ts1 (Var v) = Var (shift_elem l_ts1 v)
shift_elem :: Length ts1 -> Elem (ts1 +++ ts2) x
-> Elem (ts1 +++ t :> ts2) x
shift_elem = undefined
|
