CyclicTrees.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE LiberalTypeSynonyms #-}

module CyclicTrees where

-- inspired by
-- http://perso.ens-lyon.fr/guillaume.allais/?en/main/blog/read/cyclic-list-purely

newtype Id a = Id { getId :: a } deriving (Show, Eq)

newtype (:.:) f g a = Comp { getComp :: f (g a) } deriving (Show, Eq)

class IsId f where
  toId   :: a -> f a
  fromId :: f a -> a

instance IsId Id where
  toId   = Id 
  fromId = getId

instance (IsId f, IsId g) => IsId (f :.: g) where
  toId = Comp . toId . toId
  fromId = fromId . fromId . getComp

class Inject f g where
  inject :: f a -> g a

instance (Functor f, IsId g) => Inject f (f :.: g) where
  inject = Comp . fmap toId

instance (IsId f, Inject h g) => Inject h (f :.: g) where
  inject = Comp . toId . inject

data FPair f a b where
  FId    :: a -> b -> FPair f a b
  FLeft  :: FPair g (Functor f => a) (IsId    f => b) -> FPair (f :.: g) a b
  FRight :: FPair g (IsId    f => a) (Functor f => b) -> FPair (f :.: g) a b

type FPair' f c = FPair f c c

data CTree f a where
  CLeaf :: (forall v. f v -> v) -> CTree f a
  CRef  :: f (CTree h a) -> CTree f a
  CNode :: a
        -> FPair' f (CTree f a)
        -> CTree f a
  CRec  :: a
        -> (forall h. h (CTree (h :.: f) a)
                   -> FPair' (h :.: f) (CTree (h :.: f) a))
        -> CTree f a

type Tree a = forall f. IsId f => CTree f a

fId :: a -> b -> FPair f a b
fId = FId

leaf :: IsId f => CTree f a
leaf = CLeaf fromId

simpleNode :: a -> CTree f a -> CTree f a -> CTree f a
simpleNode a l r = CNode a (fId l r)

singleton :: IsId f => a -> CTree f a
singleton a = simpleNode a leaf leaf

cRef :: Inject f g => f (CTree g a) -> CTree g a
cRef r = CRef (inject r)

exampleA :: Tree Int
exampleA =
  simpleNode 1
    (singleton 2)
    (simpleNode 3 leaf (singleton 4))

type IdSig f a b = a -> b -> FPair f a b

exampleB :: IsId g => CTree g Int
exampleB =
  CRec 1 $ \(r :: h (CTree (h :.: g) Int)) ->
    FLeft $ (FId :: IdSig g (Functor h => CTree (h :.: g) Int)
                            (IsId h    => CTree (h :.: g) Int))
      (cRef r)
      leaf