-- Ultra-applicative: writing type-level lambda-abstractions at the value level
--
-- We show how to write even higher-order HList operations only once, in
-- one piece of code, from which value- and type- level transformations
-- will be derived by the compiler. The key is to bring the type-level
-- language closer to Haskell, in particular, by using
-- lambda-abstractions with named, humanly readable variables. We find
-- that a form of the first-class, bounded polymorphism has existed in
-- Haskell all along.
--
-- The goals of unifying value- and type-level HList programming and
-- improving error diagnosis have been set and achieved (albeit perhaps a
-- bit painfully) in Jeff Polakow's recent article:
-- Improving HList programming/debugging (longish)
-- http://www.haskell.org/pipermail/haskell-cafe/2011-January/088168.html
-- which has been the inspiration for the present code. The main
-- difference is ours use of lambda-calculus with named variables to
-- program HList operations; Jeff Polakow has used combinator calculus
-- (the point-free notation), which may become abstruse. Whereas
-- Jeff Polakow relied on GADTs to add a compiler-run--time checking, we
-- avoid GADTs, using the standard tagging approach. At least on Jeff
-- Polakow's examples, GHC reports the same error diagnostics.
-- HList programming typically requires many extensions, conventional
-- and advanced.
-- Conspicuously absent is RankNTypes: the form of first-class
-- bounded polymorphism is available in Haskell already
{-# LANGUAGE
EmptyDataDecls, TypeOperators, FlexibleInstances, FlexibleContexts,
NoMonomorphismRestriction, ScopedTypeVariables,
MultiParamTypeClasses, FunctionalDependencies, TypeFamilies,
UndecidableInstances #-}
module TypeLambdaVal where
-- ----------------------------------------------------------------------
-- We start by defining type-level booleans and HLists.
-- We aim to improve error messages and detect errors early;
-- we do not use GADTs however. Rather, we employ `type tags',
-- typical in implementations of ``dynamically typed'' languages.
-- The following HBool and HList code should be placed in a separate
-- module, with limited export: the data constructors such as Nil
-- and HCons should not be exported.
data HTrue
data HFalse
data HBool x -- the HBool type tag
hTrue :: HBool HTrue
hTrue = undefined
hFalse :: HBool HFalse
hFalse = undefined
data Nil = Nil
data x :* xs = HCons x xs
infixr 5 :*
newtype HList x = HList x -- HList type tag
-- Exported constructor functions
nil :: HList Nil
nil = HList Nil
infixr 5 *:
(*:) :: x -> HList xs -> HList (x :* xs)
x *: (HList xs) = HList (HCons x xs)
-- We should use nil, (*:) to construct the list, and the following
-- hHead, hTail to deconstruct it
hHead :: HList (x :* xs) -> x
hHead (HList (HCons x _)) = x
hTail :: HList (x :* xs) -> HList xs
hTail (HList (HCons _ xs)) = HList xs
-- Data constructors HList, HCons, Nil should not be used after this point
-- Examples of constructing and printing of an HList
{-
*TypeLambdaVal> :t 'a' *: () *: nil
'a' *: () *: nil :: HList (Char :* (() :* Nil))
*TypeLambdaVal> 'a' *: () *: nil
[<'a', ()>]
-}
-- An example of an error message upon constructing an improper HList
{-
*TypeLambdaVal> :t 1 *: ()
:1:5:
Couldn't match expected type `HList xs' against inferred type `()'
In the second argument of `(*:)', namely `()'
In the expression: 1 *: ()
-}
-- ----------------------------------------------------------------------
-- Our workhorse: the class Apply
-- It has been defined and used already in the HList library.
-- Other notable applications are
-- second-order typeclass programming
-- http://okmij.org/ftp/Haskell/types.html#poly2
-- type-level lambda-calculus
-- http://okmij.org/ftp/Haskell/types.html#computable-types
class Apply f x res | f x -> res where
apply :: f -> x -> res
-- Jeff Polakow's message also relies on Apply, calling it HEval.
-- We prefer the name Apply, because of the following, `natural' instance
instance a ~ a' => Apply (a -> b) a' b where
apply = ($)
-- ----------------------------------------------------------------------
-- Warm-up example: safe_head
-- We would like to implement the following operation on
-- ordinary lists
safe_head :: [a] -> Maybe a
safe_head lst = if null lst then Nothing else Just (head lst)
-- for HLists. The type of the result will show HNothing and HJust
-- rather than Maybe:
data HNothing = HNothing deriving Show
data HJust a = HJust a deriving Show
-- To be sure, we can write safe_head as a type class with two instances,
-- for empty and non-empty lists. For the exercise however, we would like
-- to mimic the value-level safe_head as much as possible.
-- So, we need type-level null and the type-level IF.
-- type-level null function
data HNull = HNull
instance Apply HNull (HList Nil) (HBool HTrue) where
apply _ _ = hTrue
instance Apply HNull (HList (x :* xs)) (HBool HFalse) where
apply _ _ = hFalse
hnull = apply HNull
-- Like Jeff Polakow, we do use the equality constraints
-- to improve error messages. Attempting to apply HHead to not-a-list
-- or to the empty list immediately leads to a type error.
data HHead = HHead
instance lst ~ HList (x :* xs) => Apply HHead lst x where
apply _ lst = hHead lst
-- Implementing safe_head for HLists, including taking the head of
-- HList's type, brings up a subtle point.
-- The standard Haskell function `head' is partial, which is
-- a source of much grief -- but also permitting the simple
-- safe_head code above, which includes (head lst) as a sub-expression.
-- The argument lst may well be the empty list. The type checker
-- does permit applications of `head' to a potentially empty list.
-- That application is guarded by the 'null lst' test and so
-- it will not be executed, and so safe_head is safe indeed.
-- At type-level, things are different: hHead is the total function.
-- The application to the empty HList won't type, regardless of
-- whether it will be executed.
-- Thus we need IF, the conditional expression. Unlike the conditional
-- in Jeff Polakow's message, we define ours as an applicative expression
-- that could/should be applied.
data HIF test yes no = HIF test yes no
data HIF' yes no = HIF' yes no -- auxiliary
instance (Apply test arg (HBool b),
Apply (HIF' yes no) (HBool b,arg) res)
=> Apply (HIF test yes no) arg res where
apply (HIF test yes no) arg =
apply (HIF' yes no) (apply test arg, arg)
instance Apply yes arg res => Apply (HIF' yes no) (HBool HTrue,arg) res where
apply (HIF' yes _) (_,arg) = apply yes arg
instance Apply no arg res => Apply (HIF' yes no) (HBool HFalse,arg) res where
apply (HIF' _ no) (_,arg) = apply no arg
hif test yes no = apply (HIF test yes no)
-- The first attempt at safe HList head, typical of HList programming
-- We see the usual code duplication: null checking, Maybe construction
-- is done at the value-level and, in a different form, at the type-level.
data SafeHead = SafeHead -- The label of the Apply'able function
instance (lst ~ HList lst',
Apply HNull lst (HBool b),
Apply (HIF' (lst -> HNothing)
(HList (x :* xs) -> HJust x)) (HBool b, lst) r
)
=> Apply SafeHead lst r where
apply _ lst = apply (HIF HNull ((const HNothing)::lst -> HNothing)
(\lst -> HJust (apply HHead (lst :: HList (x :* xs)))))
lst
-- Sample applications
tsh1 = apply SafeHead (1 *: nil)
-- HJust 1
tsh2 = apply SafeHead (nil)
-- HNothing
-- But we do not have to duplicate or code on two levels!
-- We skip the type-level program altogether. The following simple code
-- works just as well.
hsafe_head lst =
hif HNull (const HNothing)
(\lst -> HJust (apply HHead lst))
lst
tsh3 = hsafe_head (1 *: nil)
-- HJust 1
tsh4 = hsafe_head nil
-- HNothing
-- ----------------------------------------------------------------------
-- The main example: writing filter in terms of the right fold
-- Here is how the (value-level) filter looks for ordinary Haskell lists:
vfilter :: (a -> Bool) -> [a] -> [a]
vfilter p = foldr f []
where f x v = if p x then x : v else v
tvfilter = vfilter fst [(True,"a"), (False,"b"), (True,"")]
-- [(True,"a"),(True,"")]
-- Sample _heterogeneous_ list
l1 = (hTrue *: "a" *: () *: nil) *:
(hFalse *: 'b' *: nil) *:
(hTrue *: nil) *:
nil
-- It has the following type and the printed value
{-
*TypeLambdaVal> :t l1
l1
:: HList
(HList (HBool HTrue :* ([Char] :* (() :* Nil)))
:* (HList (HBool HFalse :* (Char :* Nil))
:* (HList (HBool HTrue :* Nil) :* Nil)))
*TypeLambdaVal> l1
[<[], [], []>]
-}
-- We need a type-level right-fold, defined as the following higher-order
-- type- and value-level function
class HFOLDR f acc xs res | f acc xs -> res where
hFoldr :: f -> acc -> HList xs -> res
instance HFOLDR f acc Nil acc where
hFoldr _ acc _ = acc
instance (HFOLDR f acc xs v,
Apply f (x,(v,())) res)
=> HFOLDR f acc (x :* xs) res
where
hFoldr f acc xs = apply f (hHead xs, (hFoldr f acc (hTail xs), ()))
-- The first, naive attempt at hFilter, similar to hsafe_head above.
-- Maybe we get lucky here as well:
hFilter1 p = hFoldr f nil
where
f (x,(v,())) = hif p (\x -> x *: v) (const v) x
-- The code type-checks. A look at the inferred type shows a trap:
{-
*TypeLambdaVal> :t hFilter1
hFilter1
:: (Apply test t (HBool b),
Apply
(HIF' (x -> HList (x :* xs)) (b1 -> HList xs)) (HBool b, t) res,
HFOLDR ((t, (HList xs, ())) -> res) (HList Nil) xs1 res1) =>
test -> HList xs1 -> res1
-}
-- into which we fall when we try to apply hFilter1:
{-
thF1 = hFilter1 HHead l1
Couldn't match expected type `HFalse' against inferred type `HTrue'
Expected type: (HList (HBool HFalse :* (Char :* Nil)),
(HList xs, ()))
Inferred type: (HList (HBool HTrue :* ([Char] :* (() :* Nil))),
(HList xs, ()))
When generalising the type(s) for `thF1'
-}
-- The type of hFilter1 can be written as
--
-- hFilter1 :: forall t x xs b1 b test xs1 res1.
-- (Apply test t (Bool b), ...) =>
-- test -> HList xs1 -> res1
--
-- or, in other words,
--
-- hFilter1 :: forall test xs1 res1.
-- (exists t x xs b1 b. Apply test t (Bool b), ...) =>
-- test -> HList xs1 -> res1
--
-- But we need
-- hFilter1 :: forall test xs1 res1.
-- (forall t x xs b1 b. Apply test t (Bool b), ...) =>
-- test -> HList xs1 -> res1
--
-- We need first-class polymorphism. Moreover, we need first-class
-- bounded polymorphism, a first-class polymorphic value with type-class
-- constraints.
-- The first solution: typical of HList, with much code duplication
-- between type- and value-levels.
-- We have to repeat Apply constraints to match the value-level expression
data FilterF p = FilterF p
instance (Apply p x (HBool b),
v ~ HList xs,
Apply
(HIF' (x -> HList (x :* xs)) (x -> v)) (HBool b, x) res)
=> Apply (FilterF p) (x,(v,())) res where
apply (FilterF p) (x,(v,())) =
hif p (\x -> (x::x) *: v) ((const v)::x -> v) (x::x)
hFilter2 p = hFoldr (FilterF p) nil
thF2 = hFilter2 HHead l1
-- The better solution, which avoids all the repetition
-- We program the lambda-calculus interpreter with human-readable
-- variable names
-- Here are these variable names, with more names to be defined later
data X = X
data V = V
-- Type-level naturals
data Z
data S n
-- The equality predicate on type-level naturals
class EQNum n1 n2 b | n1 n2 -> b
instance EQNum Z Z HTrue
instance EQNum (S n) Z HFalse
instance EQNum Z (S n) HFalse
instance EQNum n1 n2 res => EQNum (S n1) (S n2) res
class VarOrder v n | v -> n -- assign vars the total order
instance VarOrder X Z
instance VarOrder V (S Z)
-- more can be added
data Lookp v
var :: x -> Lookp x
var = undefined
newtype LAM v body = LAM body
newtype ENV v arg = ENV arg -- formal args are phantom
lam :: v -> body -> LAM v body
lam v body = LAM body
-- This one instance implements beta-redex
instance Apply body (ENV v arg) res => Apply (LAM v body) arg res where
apply (LAM body) arg = apply body ((ENV arg) :: ENV v arg)
-- compare with the type-level lambda-calculus
-- http://okmij.org/ftp/Haskell/types.html#computable-types
-- which relied on closure-conversion
-- Variable look-up in the environment
instance (VarOrder v n,
VarOrder v' n',
EQNum n n' b,
Apply (Lookp v, b) (ENV (v',vs) args) res)
=> Apply (Lookp v) (ENV (v',vs) args) res where
apply l env = apply (l, undefined::b) env
instance Apply (Lookp v, HTrue) (ENV vargs (arg,args)) arg where
apply _ (ENV (arg,_)) = arg
instance Apply (Lookp v) (ENV vs args) res
=> Apply (Lookp v, HFalse) (ENV (v',vs) (arg,args)) res where
apply (l,_) (ENV (_,args)) = apply l ((ENV args)::ENV vs args)
-- Implementing the call-by-value evaluation strategy
data A f x = A f x
instance (Apply x env xv,
Apply f env fv,
Apply fv xv res)
=> Apply (A f x) env res where
apply (A f x) env = apply (apply f env) (apply x env)
-- Ultra-applicative
-- It is quite like Control.Applicative, but applicable to
-- any thing we can apply (and we can apply more than just values
-- of the arrow type)
infixl 5 <*>
infix 6 <$>
x <*> y = A x y
x <$> y = pure x <*> y
-- The `standard library'
newtype HConst x = HConst x
instance Apply (HConst x) arg x where
apply (HConst x) _ = x
pure :: x -> HConst x
pure = HConst
data HCONS = HCONS
newtype HCONS1 x = HCONS1 x
instance Apply HCONS arg (HCONS1 arg) where
apply _ = HCONS1
instance arg ~ HList xs => Apply (HCONS1 x) arg (HList (x :* xs)) where
apply (HCONS1 x) y = x *: y
-- Finally, we can write our hFilter in terms of hFoldr
-- The code ostensibly specifies the operation on HList values. However,
-- it also specifies the corresponding operation on HList types, which we
-- can see from the inferred type of hFliter3:
hFilter3 p = hFoldr f nil
where f = lam (X,(V,()))
(HIF (p <$> var X)
(HCONS <$> var X <*> var V)
(var V))
{-
*TypeLambdaVal> :t hFilter3
hFilter3
:: (HFOLDR
(LAM
(X, (V, ()))
(HIF
(A (HConst x) (Lookp X))
(A (A (HConst HCONS) (Lookp X)) (Lookp V))
(Lookp V)))
(HList Nil)
xs
res) =>
x -> HList xs -> res
-}
-- The result of filtering has the different printed value, and the matching,
-- also filtered, type:
thF3 = hFilter3 HHead l1
{-
*TypeLambdaVal> :t thF3
thF3
:: HList
(HList (HBool HTrue :* ([Char] :* (() :* Nil)))
:* (HList (HBool HTrue :* Nil) :* Nil))
*TypeLambdaVal> thF3
[<[], []>]
-}
-- Examples of error diagnostics
{-
*TypeLambdaVal> :t hFilter3 HHead ((hTrue *: "a" *: () *: nil) *: (hFalse *: 'a' *: nil) *: hTrue *: nil)
Top level:
Couldn't match expected type `HList (HBool b :* xs)'
against inferred type `HBool HTrue'
:t hFilter3 HHead (("a" *: () *: nil) *: (hFalse *: 'a' *: nil) *: (hTrue *: nil) *: nil)
Top level:
Couldn't match expected type `HBool b'
against inferred type `[Char]'
-}
-- ----------------------------------------------------------------------
-- Showing HList nicely
instance Show (HList Nil) where
show _ = "[<>]"
instance Show x => Show (HList (x :* Nil)) where
show lst = "[<" ++ show (hHead lst) ++ ">]"
instance (Show x, Show (HList (y :* xs))) => Show (HList (x :* y :* xs)) where
show lst = let '[':'<':sxs = show (hTail lst) in
"[<" ++ show (hHead lst) ++ ", " ++ sxs
instance Show (HBool HTrue) where
show _ = "HTrue"
instance Show (HBool HFalse) where
show _ = "HFalse"