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:
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
| ^^^^^
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.