ICofree.hs

{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances     #-}

module ICofree where

data Nat = Z | S Nat

data Vec (n :: Nat) a where
  VNil  :: Vec 'Z a
  VCons :: a -> Vec n a -> Vec ('S n) a

data ICofree (n :: Nat) f a where
  (:<<) :: a -> f n (ICofree n f a) -> ICofree ('S n) f a

class Iso a b where
  toA :: b -> a
  toB :: a -> b

data IMaybe (n :: Nat) a where
  INothing :: IMaybe 'Z a
  IJust    :: a -> IMaybe ('S n) a

instance Iso (Vec n a) (ICofree n IMaybe a) where
  toA (x :<< INothing) = VCons x VNil
  toA (x :<< IJust xs) = VCons x (toA xs)

  toB (VCons x VNil)       = x :<< INothing
  toB (VCons x xs@VCons{}) = x :<< IJust (toB xs)