Experiments in Cata

Cata.hs

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}

module Program where

import Data.Foldable
import Data.Traversable
import Prelude hiding (lookup)
import Control.Monad.State
import Control.Applicative hiding (empty)
import Control.Category ((>>>), (<<<))

data Expr a = Var String
            | Lam String a
            | App a a deriving (Functor, Show, Foldable)

instance Traversable Expr where
    traverse _ (Var s) = pure (Var s)
    traverse f (Lam s e) = Lam s <$> f e
    traverse f (App e1 e2) = App <$> f e1 <*> f e2

newtype Fix f = In (f (Fix f))

out :: Fix f -> f(Fix f)
out (In f) = f

cata :: (Functor f) => (f a -> a) -> Fix f -> a
cata g = g . fmap (cata g) . out

cataM :: (Applicative m, Monad m, Traversable t) => (t a -> m a) -> Fix t -> m a
cataM f = (f =<< ) . traverse (cataM f) . out

var :: String -> Fix Expr
var = In . Var

lam :: String -> Fix Expr -> Fix Expr
lam s = In . Lam s

app :: Fix Expr -> Fix Expr -> Fix Expr
app x y = In (App x y)

expr :: Fix Expr
expr = lam "x" (lam "y" (app (app (var "+") (var "x")) (var "y")))

typeCheck :: Fix Expr -> State Int [(String, Int)]
typeCheck = cataM check
  where check :: Expr [(String, Int)] -> State Int [(String, Int)]
        check (Var s) = do i <- get
                           put (i + 1)
                           return [(s, i)]
        check (Lam s e) = do i <- get
                             put (i + 1)
                             return (("\\" ++ s, i):e)
        check (App e1 e2) = return (e1 ++ e2)


main :: IO ()
main = print (runState (typeCheck expr) 0)