Created
September 17, 2020 01:01
-
-
Save oisdk/24cfe8051c42007c8c0cf2190ac3e7bf to your computer and use it in GitHub Desktop.
This file contains 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
{-# LANGUAGE UnicodeSyntax #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
import Data.Kind | |
import Data.Functor.Const | |
data family The a :: a -> Type | |
type family Shape (a :: Type -> Type) :: k | |
class Container (c :: Type -> Type) where | |
type Position c :: Shape c -> Type | |
tabulate :: The (Shape c) n -> ∀ a. (Position c n -> a) -> c a | |
data N = Z | S N | |
data instance The N n where | |
Zy :: The N Z | |
Sy :: The N n -> The N (S n) | |
data Fin n where | |
FZ :: Fin (S n) | |
FS :: Fin n -> Fin (S n) | |
type instance Shape [] = N | |
instance Container [] where | |
type Position [] = Fin | |
tabulate Zy _ = [] | |
tabulate (Sy n) f = f FZ : tabulate n (f . FS) | |
data instance The Bool b where | |
Truey :: The Bool True | |
Falsy :: The Bool False | |
type instance Shape Maybe = Bool | |
data Factual (a :: Bool) where | |
Obvious :: Factual True | |
instance Container Maybe where | |
type Position Maybe = Factual | |
tabulate Truey f = Just (f Obvious) | |
tabulate Falsy _ = Nothing | |
data Stream a = a :< Stream a | |
type instance Shape Stream = () | |
instance Container Stream where | |
type Position Stream = Const N | |
tabulate t f = f (Const Z) :< tabulate t (f . Const . S . getConst) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment