Plucking constraints in Bluefin

#1

My latest article about Bluefin is called Plucking constraints in Bluefin.

5 Likes
#2

A nice read!

I think the type variables in the MTL plucking example are not quite right. In the final type, it should be m' everywhere.

As coherence is concerned, I think it is important that distinct effects have distinct skolemns ei. I guess this in enforced by the runST-style type of the effect plucker, wherein the skolemn occurs only in the type of the effect handle.

#3

Thanks!

Oh my, I completely garbled that type. I think this is correct fix: Fix type signature · tomjaguarpaw/H2@d824546 · GitHub. Does that match what you would expect?

I’ve deployed the change.

#4

Much better. I think it would also help to add that GHC infers the substitution m' := ExceptT String m which is why m' is no longer present in the final type. Plus, this helps to see where which constraint comes from.

#5

It already says:

for handleLengthMTL operMTL to type check we need m' to be ExceptT String m

Do you mean I should specifically say this is what GHC infers?

#6

Then it appears I just should have read more carefully :slight_smile:

1 Like
#7

You read carefully enough to find the type error, which I appreciate!