Extreme branchless: Expr without GADTs or sum-types

In the previous log we have continued my branchless journey, based on Church encoding, having this type definition:

newtype CExpr a =
  CExpr {
    runCExpr ::
      forall r.
      (a -> r a) ->
      (CExpr Int -> CExpr Int -> r Int) ->
      (CExpr Int -> CExpr Int -> r Bool) ->
      r a
  }

As a reminder, I did so to avoid relying on extensions, but, to be fair, it takes some efforts to get use to that notation.

After a second thought, well, maybe more a 20th, there is a more mainstream way to tackle it.

However, it involves embedded all operations in a product-type, leaving the implementations open, as it is done in OOP, as follows:

data FExpr a = FExpr
  { feval :: a,
    fprint :: String
  }

Thanks to GHC defaults, nothing is evaluated until it is needed.

We can define operations one by one as follows:

fval :: (Show a) => a -> FExpr a
fval x =
  FExpr
    { feval = x,
      fprint = show x
    }

fadd :: FExpr Int -> FExpr Int -> FExpr Int
fadd x y =
  FExpr
    { feval = x.feval + y.feval,
      fprint = "(" <> x.fprint <> ") + (" <> y.fprint <> ")"
    }

feq :: FExpr Int -> FExpr Int -> FExpr Bool
feq x y =
  FExpr
    { feval = x.feval == y.feval,
      fprint = "(" <> x.fprint <> ") == (" <> y.fprint <> ")"
    }

It's clearly more readable, and it makes adding new kind of expression cheap, but adding new operation costly.

We get a similar expressive power, as follows:

fexpr :: FExpr Bool
fexpr = fval 42 `feq` (fval 32 `fadd` fval 10)

-- fexpr.feval `shouldBe` True
-- fexpr.fprint `shouldBe` "(42) == ((32) + (10))"

Note: in previous logs, I have emphasized the equivalence of type-classes and records/product-types.

It could be tempting to transform previous binding in data-types and type-classes as follows:

newtype SVal a = SVal {getSVal :: a}

data SAdd f g a = SAdd {x :: f Int, y :: g Int}

data SEq f g a = SEq {x :: f Int, y :: g Int}

class SExpr (f :: Type -> Type) where
  seval :: f a -> a
  sprint :: (Show a) => f a -> String

It seems to be a great idea, until we try to define instances:

class SExpr (f :: Type -> Type) where
  seval :: f a -> a
  sprint :: (Show a) => f a -> String

instance SExpr SVal where
  seval = getSVal
  sprint = show . getSVal

instance (SExpr f, SExpr g) => SExpr (SAdd f g) where
  seval expr = seval expr.x + seval expr.y
  sprint expr = "(" <> sprint expr.x <> ") + (" <> sprint expr.y <> ")"

instance (SExpr f, SExpr g) => SExpr (SEq f g) where
  seval expr = seval expr.x == seval expr.y
  sprint expr = "(" <> sprint expr.x <> ") == (" <> sprint expr.y <> ")"

GHC will, complain, as the a in seval :: f a -> a is not constrained as follows:

test/Spec.hs:141:22-27: error: [GHC-25897]
    • Couldn't match type ‘a’ with ‘Int’
        arising from selecting the field ‘x’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          seval :: forall a. SAdd f g a -> a
        at test/Spec.hs:141:3-7
    • In the first argument of ‘seval’, namely ‘expr.x’
      In the first argument of ‘(+)’, namely ‘seval expr.x’
      In the expression: seval expr.x + seval expr.y
    • Relevant bindings include
        expr :: SAdd f g a (bound at test/Spec.hs:141:9)
        seval :: SAdd f g a -> a (bound at test/Spec.hs:141:3)
    |
141 |   seval expr = seval expr.x + seval expr.y
    |                      ^^^^^^
test/Spec.hs:145:16-43: error: [GHC-25897]
    • Couldn't match expected type ‘a’ with actual type ‘Bool’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          seval :: forall a. SEq f g a -> a
        at test/Spec.hs:145:3-7
    • In the expression: seval expr.x == seval expr.y
      In an equation for ‘seval’:
          seval expr = seval expr.x == seval expr.y
      In the instance declaration for ‘SExpr (SEq f g)’
    • Relevant bindings include
        expr :: SEq f g a (bound at test/Spec.hs:145:9)
        seval :: SEq f g a -> a (bound at test/Spec.hs:145:3)
    |
145 |   seval expr = seval expr.x == seval expr.y
    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

It cannot be solved, unless we rely on TypeFamilies to enforce the output, as follows:

class SExpr (f :: Type -> Type) where
  type Out f :: Type -> Type
  seval :: f a -> Out f a
  sprint :: (Show a) => f a -> String

We can try to implement the instances relying on Identity/Const again as follows:

instance SExpr SVal where
  type Out SVal = Identity
  seval = Identity . getSVal
  sprint = show . getSVal

instance (SExpr f, SExpr g) => SExpr (SAdd f g) where
  type Out (SAdd f g) = Const Int
  seval expr = Const $ seval expr.x + seval expr.y
  sprint expr = "(" <> sprint expr.x <> ") + (" <> sprint expr.y <> ")"

instance (SExpr f, SExpr g) => SExpr (SEq f g) where
  type Out (SEq f g) = Const Bool
  seval expr = Const $ seval expr.x == seval expr.y
  sprint expr = "(" <> sprint expr.x <> ") == (" <> sprint expr.y <> ")"

But it won't work either, as seval produces a wrapped value.

We need to make a helper so everything holds:

class Extractable a where
  type Extracted a :: Type
  extract :: a -> Extracted a

instance Extractable (Identity a) where
  type Extracted (Identity a) = a
  extract = runIdentity

instance Extractable (Const a b) where
  type Extracted (Const a b) = a
  extract = getConst

And, with the glorious UndecidableInstances, we can write type-checking instances as follows:

instance
  ( SExpr f,
    SExpr g,
    Extractable (Out f Int),
    Extractable (Out g Int),
    Extracted (Out f Int) ~ Int,
    Extracted (Out g Int) ~ Int
  ) =>
  SExpr (SAdd f g)
  where
  type Out (SAdd f g) = Const Int
  seval expr = Const $ extract (seval expr.x) + extract (seval expr.y)
  sprint expr = "(" <> sprint expr.x <> ") + (" <> sprint expr.y <> ")"

instance
  ( SExpr f,
    SExpr g,
    Extractable (Out f Int),
    Extractable (Out g Int),
    Extracted (Out f Int) ~ Int,
    Extracted (Out g Int) ~ Int
  ) =>
  SExpr (SEq f g)
  where
  type Out (SEq f g) = Const Bool
  seval expr = Const $ extract (seval expr.x) == extract (seval expr.y)
  sprint expr = "(" <> sprint expr.x <> ") == (" <> sprint expr.y <> ")"

Quite ugly, but we keep the same expressiveness, with a bonus of having the expression structure at type-level, as follows:

sexpr :: SEq SVal (SAdd SVal SVal) Bool
sexpr = SVal 42 `SEq` (SVal 32 `SAdd` SVal 10)

-- getConst (seval sexpr) `shouldBe` True
-- sprint sexpr `shouldBe` "(42) == ((32) + (10))"

We tend to overlook plain data-types over type-classes for various reason.

But type-classes can be too rigid in some cases, and we should get back to more basic constructs.