gistfile1.txt

{-# LANGUAGE 
  GADTs,
  FlexibleInstances, FlexibleContexts, UndecidableInstances,
  StandaloneDeriving, TypeOperators, Rank2Types,
  MultiParamTypeClasses, ConstraintKinds,
  DeriveTraversable, DeriveFunctor, DeriveFoldable,
  TypeFamilies, FunctionalDependencies, 
  ScopedTypeVariables, GeneralizedNewtypeDeriving
 #-}

import Control.Compose
import Control.Monad
import Control.Monad.State
import Control.Monad.Writer
import Control.Monad.Identity
import Control.Monad.Error
import Data.Hashable

{- Higher order functors
   from http://www.timphilipwilliams.com/posts/2013-01-16-fixing-gadts.html
-}

newtype HFix h a = HFix { unHFix :: h (HFix h) a }
instance (Show (h (HFix h) a)) => Show (HFix h a) where
  show = parens . show . unHFix where
    parens x = "(" ++ x ++ ")"

-- Natural transformation
type f :~> g = forall a. f a -> g a

-- Higher order functor
class HFunctor (h :: (* -> *) -> * -> *) where
    hfmap :: (f :~> g) -> h f :~> h g

-- Higher order catamorphism
hcata :: HFunctor h => (h f :~> f) -> HFix h :~> f
hcata alg = alg . hfmap (hcata alg) . unHFix

-- Standard Functors
newtype I x = I { unI :: x } deriving Show
newtype K x y = K { unK :: x }

{- Example: Tree with Peano numerals in the nodes -}
data Tree where
data Nat where
deriving instance Show Tree
deriving instance Show Nat
deriving instance (Show (r a), Show (r Tree), Show (r Nat)) => Show (ExprF r a)
  
data ExprF :: (* -> *) -> * -> * where
  Tip :: ExprF r Tree
  Bin :: r Tree -> r Nat -> r Tree -> ExprF r Tree
  Zero :: ExprF r Nat
  Succ :: r Nat -> ExprF r Nat
type Expr = HFix ExprF

--deriving instance Show (ExprF a b)
--deriving instance (Show r a) => Show (ExprF r a)
--deriving instance (Show a) => Show (ExprF (K a) b)

instance HFunctor ExprF where
  hfmap f Tip = Tip
  hfmap f (Bin l a r) = Bin (f l) (f a) (f r)
  hfmap f Zero = Zero
  hfmap f (Succ n) = Succ (f n)





class (HFunctor f, Monad m) => Monadic f d m where
  construct :: forall a. f d a -> m (d a)
  destruct  :: forall a.   d a -> m (f d a)

-- Distributive law requirement here?
-- Laws:
--     forall f. construct <=< destruct . hfmap

instance (HFunctor f) => Monadic f (HFix f) Identity where
  construct = return . HFix
  destruct = return . unHFix


{- Example of a tree with peano numbers in the nodes -}

{-instance (forall a. Show (HFix f a)) => Monadic f (HFix f) IO where
  construct (HFix x) = do { print ("Cnst", x) ; return x }
  destruct  = m . unHFix where m x = do { print ("Dstr", x) ; return x }
-}

instance Monadic ExprF (HFix ExprF) IO where
  construct = m . HFix   where m x = do { print ("Cnst", x) ; return x }
  destruct  = m . unHFix where m x = do { print ("Dstr", x) ; return x }

compare' :: HFix ExprF Nat -> HFix ExprF Nat -> Ordering
compare' (HFix Zero) (HFix Zero) = EQ
compare' (HFix Zero) _ = LT
compare' _ (HFix Zero) = GT
compare' (HFix (Succ a)) (HFix (Succ b)) = compare' a b

compareM :: Monadic ExprF d m => (d Nat) -> (d Nat) -> m Ordering
compareM a' b' = do
  a :: ExprF d Nat <- destruct a'
  b :: ExprF d Nat <- destruct b'
  cmp a b where
    cmp Zero Zero = return EQ
    cmp Zero _    = return LT
    cmp _ Zero    = return GT
    cmp (Succ a) (Succ b) = compareM a b

lookupM :: Monadic ExprF d m => (d Nat) -> (d Tree) -> m Bool
lookupM a = look where
  look = (=<<) look' . destruct
  look' Tip = return False
  look' (Bin l b r) = compareM a b >>= look'' where
      look'' EQ = return True
      look'' LT = look l
      look'' GT = look r

type D = Int
{-instance (HFunctor f, forall a. MonadWriter [f (K D) a] m, Hashable (f (K D) a)) => Monadic f (HFix f) m where
  construct = return . HFix
  destruct (HFix e) = do
--    tell [hfmap (hcata hash) e]
    return e
-}

-- Examples

data Tree' = Tip' | Bin' Tree' Int Tree' deriving Show

toTree :: Expr a -> Either Tree' Int
toTree = unK . hcata alg where
    alg :: ExprF (K (Either Tree' Int)) :~> K (Either Tree' Int)
    alg Zero                 = K $ Right 0
    alg (Succ (K (Right n))) = K $ Right (n+1)
    alg Tip                  = K $ Left Tip'
    alg (Bin (K (Left l))
             (K (Right a))
             (K (Left r)))   = K $ Left (Bin' l a r)

fromInt 0 = HFix Zero
fromInt n = HFix . Succ $ fromInt (n-1)

tip = HFix Tip
bin l a r = HFix $ Bin l (fromInt a) r

-- Test tree
t0 = bin (bin tip 0 tip) 1 (bin tip 2 tip)

-- Assert equal
test1 = runIdentity $ compareM (fromInt 2) (fromInt 2)

main = do
  (=<<) print $ lookupM (fromInt 0) t0
  (=<<) print $ lookupM (fromInt 3) t0