Last active
May 8, 2021 20:56
-
-
Save Russoul/0a22b8e82ddc201af4adbc99b0b76fe5 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| %default total | |
| data Use = None | Once | Many | |
| %hide Prelude.Num.(*) | |
| %hide Prelude.Num.(+) | |
| %hide Prelude.List | |
| %hide Prelude.(::) | |
| %hide Prelude.Nil | |
| %hide Prelude.map | |
| %hide List.length | |
| %hide Prelude.Nat | |
| %hide Prelude.Z | |
| %hide Prelude.S | |
| %hide Builtin.fst | |
| (*) : Use -> Use -> Use | |
| Once * x = x | |
| Many * None = None | |
| Many * _ = Many | |
| None * _ = None | |
| (+) : Use -> Use -> Use | |
| None + x = x | |
| Once + None = Once | |
| Once + _ = Many | |
| Many + _ = Many | |
| data M : Use -> Type -> Type where | |
| U : (x : a) -> M Many a | |
| L : (1 x : a) -> M Once a | |
| E : (0 x : a) -> M None a | |
| namespace Axiom | |
| ||| Linear contraction. | |
| ||| This is the only cheaty part. | |
| ||| You can't normally write this definition with `r, k` erased. | |
| ||| Otherwise, it can be easily done, as in the commented out lines. | |
| ||| At runtime this could be just a `dup`, due to the newtype optimisation. | |
| ||| It won't compute in proofs but we don't need that in `map`. | |
| export | |
| contr : {0 r, k : _} -> (1 x : M (r + k) a) -> LPair (M r a) (M k a) | |
| -- contr {r = None} {k = None} (E x) = (E x) # (E x) | |
| -- contr {r = None} {k = Once} (L x) = (E x) # (L x) | |
| -- contr {r = None} {k = Many} (U x) = (E x) # (U x) | |
| -- contr {r = Once} {k = None} (L x) = (L x) # (E x) | |
| -- contr {r = Once} {k = Once} (U x) = (L x) # (L x) | |
| -- contr {r = Once} {k = Many} (U x) = (L x) # (U x) | |
| -- contr {r = Many} {k = None} (U x) = (U x) # (E x) | |
| -- contr {r = Many} {k = Once} (U x) = (U x) # (L x) | |
| -- contr {r = Many} {k = Many} (U x) = (U x) # (U x) | |
| data Nat : Type where | |
| Z : Nat | |
| S : (1 x : Nat) -> Nat | |
| plus : (1 x : Nat) -> (1 y : Nat) -> Nat | |
| plus Z y = y | |
| plus (S x) y = S (plus x y) | |
| data List : Type -> Type where | |
| Nil : List a | |
| (::) : (1 x : a) -> (1 xs : List a) -> List a | |
| forget : Nat -> Use | |
| forget Z = None | |
| forget (S Z) = Once | |
| forget _ = Many | |
| forgetPlusHomo : (p, k : Nat) -> forget (p `plus` k) === forget p + forget k | |
| forgetPlusHomo Z Z = Refl | |
| forgetPlusHomo Z (S Z) = Refl | |
| forgetPlusHomo Z (S (S _)) = Refl | |
| forgetPlusHomo (S Z) Z = Refl | |
| forgetPlusHomo (S Z) (S Z) = Refl | |
| forgetPlusHomo (S Z) (S (S _)) = Refl | |
| forgetPlusHomo (S (S _)) Z = Refl | |
| forgetPlusHomo (S (S _)) (S Z) = Refl | |
| forgetPlusHomo (S (S _)) (S (S _)) = Refl | |
| 0 | |
| length0 : (1 xs : List a) -> Nat | |
| length0 [] = Z | |
| length0 (x :: xs) = S Z `plus` length0 xs | |
| transport : forall p. (0 i : x === y) -> (1 px : p x) -> p y | |
| transport Refl x = x | |
| mutual | |
| mapH : (1 x : a) | |
| -> (1 xs : List a) | |
| -> (1 f'' : LPair (M Once $ (1 x : a) -> b) (M (forget (length0 xs)) ((1 x : a) -> b))) | |
| -> List b | |
| mapH x xs (L f # f'') = f x :: map xs f'' | |
| ||| A regular functorial map, with a dependent multiplicity in the function signature. | |
| map : (1 xs : List a) -> (1 f : M (forget (length0 xs)) ((1 x : a) -> b)) -> List b | |
| map [] (E f) = [] | |
| map (x :: xs) f = | |
| let f' = transport {p = \l => M l ((1 _ : a) -> b)} (forgetPlusHomo (S Z) (length0 xs)) f | |
| f'' = contr {r = Once, k = forget (length0 xs)} f' in | |
| mapH x xs f'' | |
| testMap : List Int | |
| testMap = let | |
| many = map [1, 2, 3] ?many | |
| once = map [1] ?one | |
| none = map [] ?none | |
| in ?w |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment