gistfile1.hs

{-# LANGUAGE GADTs, ExistentialQuantification, ImpredicativeTypes #-}

module Gadtalgebra where
  
import Data.Char

data Term a where
  Const  :: a -> Term a
  Plus   :: Term Int -> Term Int -> Term Int
  Pair   :: Term b -> Term c -> Term (b,c)
  App    :: Term (b -> a) -> Term b -> Term a

newtype Foo a = Foo a deriving Show
  
type TermAlgebra f =  ( (forall a.    a -> f a)
                      , f Int -> f Int -> f Int
                      , forall b c.  f b -> f c -> f (b,c)
                      , forall a b.  f (b -> a) -> f b -> f a
                      )

foldTerm :: TermAlgebra f -> Term a -> f a
foldTerm ta@(c,pl, p, a) (Const v) = c v
foldTerm ta@(c,pl, p, a) (Plus  p1 p2) = pl (foldTerm ta p1)
                                            (foldTerm ta p2)

foldTerm ta@(c,pl, p, a) (Pair  x y) = p (foldTerm ta x)
                                         (foldTerm ta y)
foldTerm ta@(c,pl, p, a) (App   f x) = a (foldTerm ta f)
                                         (foldTerm ta x)
     
     
sample = (Const 4 `Plus` Const 8) `Plus` (Const 3 `Plus` Const 5)                                 
                                      
calc = foldTerm (Const, Plus, Pair, App)