Last active
March 9, 2021 13:07
-
-
Save Mr-Andersen/5139324140837f843f330ef7f2ea9667 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
| -- Works (no `List` at all) ------------------------------------------------------ | |
| data Layers2 : Nat -> Type -> Type where | |
| Leaf2 : t -> Layers2 lvl t | |
| Node2 : Layers2 (S lvl) t -> Layers2 (S lvl) t -> Layers2 lvl t | |
| total | |
| mapLayers2 : (a -> b) -> Layers2 lvl a -> Layers2 lvl b | |
| mapLayers2 f (Leaf2 x) = Leaf2 (f x) | |
| mapLayers2 f (Node2 left right) = Node2 (mapLayers2 f left) (mapLayers2 f right) | |
| -- Doesn't work (`List`) --------------------------------------------------------- | |
| data Layers : Nat -> Type -> Type where | |
| Leaf : t -> Layers lvl t | |
| Node : List (Layers (S lvl) t) -> Layers lvl t | |
| total | |
| mapLayers : (a -> b) -> Layers lvl a -> Layers lvl b | |
| mapLayers f (Leaf x) = Leaf (f x) | |
| mapLayers f (Node kids) = Node (mapLayers f <$> kids) | |
| -- Works (`List` is replaced with `LayersNode`) ---------------------------------- | |
| mutual | |
| data Layers : Nat -> Type -> Type where | |
| Leaf : t -> Layers lvl t | |
| -- Node : List (Layers (S lvl) t) -> Layers lvl t | |
| Node : LayersNode lvl t -> Layers lvl t | |
| data LayersNode : Nat -> Type -> Type where | |
| Nil : LayersNode lvl t | |
| (::) : Layers (S lvl) t -> LayersNode lvl t -> LayersNode lvl t | |
| mutual | |
| total | |
| mapLayers : (a -> b) -> Layers lvl a -> Layers lvl b | |
| mapLayers f (Leaf x) = Leaf (f x) | |
| mapLayers f (Node kids) = Node (mapLayersNode f kids) | |
| total | |
| mapLayersNode : (a -> b) -> LayersNode lvl a -> LayersNode lvl b | |
| mapLayersNode f [] = [] | |
| mapLayersNode f (x::xs) = (mapLayers f x) :: (mapLayersNode f xs) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment