Representable functors, sized vectors and finite sets

representable.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
type Nat f g = forall x. f x -> g x
type Hom a b = a -> b

class Indexable f where 
    type family IxTy f :: *
    index :: f a -> IxTy f -> a

data List a = Nil | Cons a (List a)
instance Indexable List where
    type IxTy List = Int
    index (Cons a as) 0 = a 
    index (Cons a as) n = index as (n-1)


data BinaryTree a = Leaf a | Branch (BinaryTree a) (BinaryTree a)
data Path = L Path | R Path | Done

instance Indexable BinaryTree where
    type IxTy BinaryTree = Path
    index (Leaf a) Done = a
    index (Branch l _) (L path) = index l path
    index (Branch _ r) (R path) = index r path

-- Functor f is representable iff isomorphic to SOME hom functor
-- f: C -> Set -- set to be isomorphic to hom functor
-- ∃d∈C, f ~= Hom(d, -)
-- d is called as the "representing object" of functor f
-- functor f: Type -> Type
-- d st f ~= Hom d
-- f x ~= Hom d x
-- f x ~= d -> x
-- f  -> Hom d
-- Hom d  -> Hom f
class Functor f => Representable f where
    type family RepresentingObj f :: *
    -- fwd :: Nat f (Hom d)
    -- fwd :: forall x. f x ->  (Hom d) x
    fwd :: forall x. f x ->  (RepresentingObj f -> x) 
    -- index :: forall x. f x ->  (d -> x) 
    -- index = fwd
    -- bwd :: Nat (Hom d) f
    -- bwd :: forall x. (Hom d x) -> f x
    bwd :: forall x. (RepresentingObj f -> x) -> f x -- memoization
    tabulate :: forall x. (RepresentingObj f -> x) -> f x -- memoization
    tabulate = bwd


-- | always infinite stream
data Stream a = SCons a (Stream a)

instance Functor Stream where
    fmap f (SCons x xs) = SCons (f x) (fmap f xs)
instance Representable Stream where
    type RepresentingObj Stream = Int
    fwd (SCons x _) 0 = x
    fwd (SCons _ xs) n = fwd xs (n-1)

    bwd int2x = go 0 where
        -- go :: Int -> Stream a
        go n = SCons (int2x n) (go (n+1))

data NAT = ZERO | SUCC NAT deriving(Eq)

countNAT :: NAT -> Int
countNAT ZERO = 0
countNAT (SUCC n) = countNAT n + 1

instance Show NAT where show n = "n-" ++ show (countNAT n)

-- FinSet 10: exactly 10 values
data FinSet (n :: NAT) where
    Intros :: FinSet (SUCC n)
    Lift :: FinSet n -> FinSet (SUCC n)

data Vector (n :: NAT) (a :: *)  where
    VNil :: Vector ZERO a
    VCons :: a -> Vector n a -> Vector (SUCC n) a

instance Functor (Vector n) where
    fmap _ VNil = VNil
    fmap f (VCons a as) = VCons (f a) (fmap f as)


tabulateVec :: (FinSet n -> x) -> Vector n x
tabulateVec = error "exercise for the reader"

instance Representable (Vector n) where
    type RepresentingObj (Vector n) = FinSet n

    -- fwd :: forall x. f x ->  (RepresentingObj f -> x) 
    fwd :: forall x. Vector n x -> ((FinSet n) -> x)
    fwd (VCons x xs) Intros = x
    fwd (VCons x xs) (Lift n) = fwd xs n

    bwd :: forall x. ((FinSet n) -> x) -> Vector n x
    bwd finset2x = 

countFinSet :: FinSet n -> Int
countFinSet Intros = 1
countFinSet (Lift x) = 1 + countFinSet x

instance Show (FinSet n) where
    show x =  "[" ++ show (countFinSet x) ++ " <:" ++  "???" ++ "]" where
-- 
-- FinSet ONE
-- - Intros :: FinSet ONE : 1
--
-- FinSet (SUCC ONE)
--  - Intros :: FinSet (SUCC ONE) : 1
--  - Lift (Intros :: FinSet ONE) :: FinSet (SUCC ONE) : 2
--
-- FinSet (SUCC (SUCC ONE))
--  - Intros :: FinSet (SUCC (SUCC ONE))
--  - Lift (Intros :: FinSet ONE) :: FinSet (SUCC ONE)