Avoid boilerpate of tagless final in Haskell

Question

The following code shows a tagless final lambda typeclass and an evaluation instance:

class Lambda (repr :: * -> *) where
    int :: Int -> repr Int
    add :: repr Int -> repr Int -> repr Int
    lambda :: forall a b. (repr a -> repr b) -> repr (a -> b)
    apply :: forall a b. repr (a -> b) -> repr a -> repr b

-- eval
instance Lambda Identity where
    int = Identity
    add x y = Identity $ runIdentity x + runIdentity y
    lambda f = Identity $ \x -> runIdentity (f (Identity x))
    apply (Identity f) (Identity x) = Identity $ f x

But there are lots of boilerplate of plugging Identity and runIdentity. How can I avoid them?

I tried to use the type family as following:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}

class Lambda f where
    type Repr f a
    int :: Int -> Repr f Int
    add :: Repr f Int -> Repr f Int -> Repr f Int
    lambda :: forall a b. (Repr f a -> Repr f b) -> Repr f (a -> b)
    apply :: forall a b. Repr f (a -> b) -> Repr f a -> Repr f b
    
data Eval
instance Lambda Eval where
    type Repr Eval a = a
    int = id
    add = (+)
    lambda = id
    apply f = f

I have two questions:

Why is the following declaration incurs an error?

exp1 :: Lambda f => Repr f Int
exp1 = int 1

with error:

app/Main.hs:63:8: error:
    • Couldn't match expected type: Repr f Int
                  with actual type: Repr f0 Int
      NB: ‘Repr’ is a non-injective type family
      The type variable ‘f0’ is ambiguous
    • In the expression: int 1
      In an equation for ‘exp1’: exp1 = int 1
    • Relevant bindings include
        exp1 :: Repr f Int (bound at app/Main.hs:63:1)
   |
63 | exp1 = int 1
   |        ^^^^^

Is it a good practice to write the tagless final with the type family?

chi · Answer 1 · 2023-03-26T21:09:27.883

You could try using "safe coercions":

import Data.Coerce

instance Lambda Identity where
    int = Identity
    add = coerce ((+) @Int)
    lambda f = coerce f
    apply f x = coerce f x

Intuitively coerce is a tool that will automagically apply Identity and runIdentity as needed to make the expression to type-check. Note that it will usually fail to work if you use it on a polymorphic function since type inference won't be able to work as usual: that's why we wrote coerce ((+) @Int) above.

More in detail, you can convince yourself that coerce is enough in the above cases if you compare types before and after coercion, and observe that it only differs from Identity being used at some points.

add = coerce ((+) @Int)
-- before :: Int -> Int -> Int
-- after  :: Identity Int -> Identity Int -> Identity Int

lambda f = coerce f
-- before :: Identity a -> Identity b
-- after  :: Identity (a -> b)

apply f x = coerce f x
-- f before :: Identity (a -> b)
--   after  :: Identity a -> Identity b

Anyway, using type families instead as you did looks good to me. Regarding your question

Why is the following declaration incurs an error?
exp1 :: Lambda f => Repr f Int
exp1 = int 1

This raises an error because the call of int is ambiguous. That could be the int defined in the constraint Lambda f, but it could also be the int defined in Lambda Eval (i.e., we do not use the constraint in scope). Note that it is possible that two instances have the same Repr because type families do not have to be injective, so the ambiguity arises. For example:

data Eval
instance Lambda Eval where
    type Repr Eval a = a
    int = id
    ...
data Eval2
instance Lambda Eval2 where
    type Repr Eval a = a
    int = (+10)
    ...

test :: Repr Eval Int -- AKA Int
test = int 7 -- is it 7 or 17 ? It's ambiguous, so we reject it.

To disambiguate, use ScopedTypeVariables and TypeApplications.

exp1 :: forall f. Lambda f => Repr f Int
exp1 = int @f 1   -- use the int from the constraint

Is it a good practice to write the tagless final with the type family?

Here I must confess that I'm not too familiar with the tagless final approach, so I can't give you a precise answer. I can only state that it does not look wrong in my eye.

Avoid boilerpate of tagless final in Haskell

1 Answers1