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 )
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 )
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.