container.hs

{-# 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)