Skip to content

Instantly share code, notes, and snippets.

@oisdk

oisdk/container.hs

Created Sep 17, 2020
Embed
What would you like to do?
{-# 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
You can’t perform that action at this time.