{-# Language RankNTypes #-}
{-# Language NoMonomorphismRestriction #-}
-- * A short overview of the Tagless-Final approach and of
-- * the Boehm-Beraducci's encoding (and NBE)
module BB where
-- * Standard integer lists
data List = Nil | Cons Int List
l1 = Cons 2 (Cons 3 (Cons 4 Nil))
-- Standard fold (with slightly rearranged arguments)
fold :: List -> (a,Int -> a -> a) -> a
fold Nil (z,f) = z
fold (Cons h t) (z,f) = f h (fold t (z,f))
-- * Evaluators are folds
sumI l = fold l (0,(+))
_ = sumI l1
prodI l = fold l (1,(*))
_ = prodI l1
viewI l =
"[" ++ fold l ("]",\h a -> show h ++ (if a == "]" then a else ","++a))
_ = viewI l1
-- Look at the ubiquitous (fold l)! We can represent a list by (fold List)
type ListF = forall a. (a,Int -> a -> a) -> a
nil :: ListF
nil (z,f) = z
cons :: Int -> ListF -> ListF
cons h l (z,f) = f h (l (z,f))
-- * Just like l1 but with lower case
l2 = cons 2 (cons 3 (cons 4 nil))
-- Like sumI but without fold
sumF l = l (0,(+))
_ = sumF l2
prodF l = l (1,(*))
_ = prodF l2
viewF l =
"[" ++ l ("]",\h a -> show h ++ (if a == "]" then a else ","++a))
_ = viewF l2
-- * Tagless-final hides the (z,f) argument by various means
class LST r where
nl :: r
cs :: Int -> r -> r
-- Just like l1 but with lower case
l3 :: LST r => r
l3 = cs 2 (cs 3 (cs 4 nl))
newtype Sum = Sum Int
instance LST Sum where
nl = Sum 0
cs h (Sum l) = Sum $ h + l
sumT :: Sum -> Int
sumT (Sum a) = a
_ = sumT l3
-- The hiding has the benefit of extensibility (Haskell takes care of that)
-- * Using Tagless-Final in other languages likewise takes advantage
-- * of the language facilities to hide the `dictionary' passing and
-- * make it extensible. (E.g., OCaml modules, Scala's traits)
-- * //
-- * Representing a data type by its fold.
-- * Church encoding?
-- * http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html
-- First, it is typed. Second, Church (Kleene) did not show
-- any systematic way to deconstruct data types
-- (even the notion of data types did not exists back then)
-- * The second part lets us deal with operations that are not folds
-- * Tagless-final optimizations are very similar (but not identical!)
-- * to the Boehm-Beraducci's construction
-- * We also work with non-strictly positive data types