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 :: GExpr Bool
gexpr = Val 42 `Eq` (Val 32 `Add` Val 10)

We can write a small evaluator keeping the type-level parametric type, as follows:

geval :: GExpr a -> a
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' a
nothing = Maybe' const

just :: a -> Maybe' a
just x = Maybe' $ \_ f -> f x

fromMaybe' :: a -> Maybe' a -> a
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 {
    runCExpr ::
      forall r.
      (a -> r a) ->
      (CExpr Int -> CExpr Int -> r Int) ->
      (CExpr Int -> CExpr Int -> r Bool) ->
      r a
  }

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 :: a -> CExpr a
val x = CExpr $ \f _ _ -> f x

add :: CExpr Int -> CExpr Int ->  CExpr Int
add x y = CExpr $ \_ f _ -> f x y

eq :: CExpr Int -> CExpr Int ->  CExpr Bool
eq x y = CExpr $ \_ _ f -> f x y

We get a similar expressive power, as follows:

cexpr :: CExpr Bool
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 :: CExpr a -> a
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 :: Show a => CExpr a -> String
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))"