Extreme branchless: Expr without GADTs
It's been a while since I have closed my branchless journey. Actually, I have only suspended the writing about it.
About 5 years ago, I was teaching functional programming in a local engineering.
Students had several projects, including one which was to build a small compiler.
They had to use Haskell 98, without extensions.
At some point, while I was interviewing a pair of students, they complained they had to use unsafe functions (error
and undefined
) to silent some non-exhaustive pattern-matching when dealing with the algebraic data-types representing the AST of the program.
I have said that there was a way, but it was requiring an extension: GADTs.
As a reminder, in classical Algebraic Data-Types (ADTs), all constructors have a type derived from its values.
Take the following examples:
data Maybe a = Nothing | Just a
Just True :: Maybe Bool
Nothing :: Mabe a -- 'a' is not held by the constructor, it is polymorphic
In Generalized Algebraic Data-Types (GADTs), we can bind parametric types, such as the following type:
data GExpr a where
Val :: a -> GExpr a
Add :: GExpr Int -> GExpr Int -> GExpr Int
Eq :: GExpr Int -> GExpr Int -> GExpr Bool
In Val
, the parametric type, of GExpr
is bound by the constructor, but in Add
and Eq
, they are not, acting as Phantom types, which can be bound freely.
I get then a small eDSL which prevents ill-typed expressions:
gexpr = Val 42 `Eq` (Val 32 `Add` Val 10)
We can write a small evaluator keeping the type-level parametric type, as follows:
geval =
\case
Val x -> x
Add x y -> geval x + geval y
Eq x y -> geval x == geval y
-- geval gexpr `shouldBe` True
In the previous logs, we have seen how to turn the here-above definition of Maybe
into a function using Church encoding as follows:
newtype Maybe' a =
Maybe' { runChurchMaybe :: forall r. r -> (a -> r) -> r }
nothing = Maybe' const
just x = Maybe' $ \_ f -> f x
fromMaybe' def maybe' = runChurchMaybe maybe' def id
It took me a while to figure-out how to be one-step further integrating GADTs.
The trick was to parameterize r
as follows:
newtype CExpr a =
CExpr {
}
GADTs in Church encoding are not distinct to regular parameterized ADTs, it is trivial.
We have to define each constructor with calling functions relevant to each constructor as follows:
val x = CExpr $ \f _ _ -> f x
add x y = CExpr $ \_ f _ -> f x y
eq x y = CExpr $ \_ _ f -> f x y
We get a similar expressive power, as follows:
cexpr = val 42 `eq` (val 32 `add` val 10)
There is a down-side of this as, when defining an evaluator, I have to wrap it in a parameterized type as follows:
ceval exp =
runIdentity $
runCExpr
exp
return
(\x y -> return $ ceval x + ceval y)
(\x y -> return $ ceval x == ceval y)
-- newtype Identity a = Identity { runIdentity :: a }
-- ceval cexpr `shouldBe` True
It is great is we want to keep track of the type, but if we want to ignore it, for example to display the expression, we have to rely on a wrapper with a phantom type, as follows:
cprint exp =
getConst $
runCExpr
exp
(Const . show)
(\x y -> Const $ "(" <> cprint x <> ") + (" <> cprint y <> ")")
(\x y -> Const $ "(" <> cprint x <> ") == (" <> cprint y <> ")")
-- newtype Const a b = Const { getConst :: a }
-- cprint cexpr `shouldBe` "(42) == ((32) + (10))"