diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-02-07 08:28:27 +0100 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-02-07 21:36:23 +0100 |
commit | 88cedb5412b3f2b921debb40866d53224341fe75 (patch) | |
tree | e88e41e11772e279f6d445b085be63daf081a78a /lc/Internals.lc | |
parent | 6e291f28363cc873b809e020eef8a929c8244508 (diff) |
refactoring
Diffstat (limited to 'lc/Internals.lc')
-rw-r--r-- | lc/Internals.lc | 23 |
1 files changed, 15 insertions, 8 deletions
diff --git a/lc/Internals.lc b/lc/Internals.lc index 15d1a38e..72386f16 100644 --- a/lc/Internals.lc +++ b/lc/Internals.lc | |||
@@ -13,6 +13,14 @@ data Unit = TT | |||
13 | data String | 13 | data String |
14 | data Empty (a :: String) | 14 | data Empty (a :: String) |
15 | 15 | ||
16 | unsafeCoerce :: forall a b . a -> b | ||
17 | |||
18 | -- equality constraints | ||
19 | type family EqCT (t :: Type) (a :: t) (b :: t) | ||
20 | {- | ||
21 | coe :: forall (a :: Type) (b :: Type) -> EqCT Type a b -> a -> b | ||
22 | coe a b TT x = unsafeCoerce @a @b x | ||
23 | -} | ||
16 | -- TODO: generate? | 24 | -- TODO: generate? |
17 | data Tuple0 = Tuple0 | 25 | data Tuple0 = Tuple0 |
18 | data Tuple1 a = Tuple1 a | 26 | data Tuple1 a = Tuple1 a |
@@ -39,16 +47,15 @@ type family T2 a b | |||
39 | 47 | ||
40 | match'Type :: forall (m :: Type -> Type) -> m Type -> forall (t :: Type) -> m t -> m t | 48 | match'Type :: forall (m :: Type -> Type) -> m Type -> forall (t :: Type) -> m t -> m t |
41 | 49 | ||
42 | --testmt :: forall (t :: Type) -> t -> t | 50 | testmt :: forall (t :: Type) -> t -> t |
43 | --testmt 'Type = \'Tuple0 -> 'Tuple0 | 51 | testmt 'Type = \'Tuple0 -> 'Tuple0 |
44 | 52 | --testmt t x = (match'Type (\q -> (q -> q)) (\x -> match'Tuple0 (\q -> & 'Type) 'Tuple0 x undefined) t undefined) x | |
45 | -- equality constraints | 53 | --testmt t x = (match'Type (\q -> (q -> q)) (\x -> match'Tuple0 (\q -> 'Type) 'Tuple0 x undefined) t undefined) x |
46 | type family EqCT (t :: Type) (a :: t) (b :: t) | ||
47 | 54 | ||
48 | --type instance EqCT Type Type Type = Unit--(a, b) (JoinTupleType a' b') = T2 (EqCT Type a a') (EqCT Type b b') | 55 | --type instance EqCT Type = \'Type 'Type -> 'Unit |
49 | --type instance EqCT Type (a, b) (JoinTupleType a' b') = T2 (EqCT Type a a') (EqCT Type b b') | 56 | --type instance EqCT Type = \'(a, b) '(JoinTupleType a' b') -> '(T2 (EqCT Type a a') (EqCT Type b b')) |
50 | 57 | ||
51 | type EqCTt = EqCT Type | 58 | type EqCTt = EqCT _ |
52 | 59 | ||
53 | -- builtin conjuction of constraint witnesses | 60 | -- builtin conjuction of constraint witnesses |
54 | t2C :: Unit -> Unit -> Unit | 61 | t2C :: Unit -> Unit -> Unit |