Haskell Interlude 53: Garrett Morris

Links
#1

In this episode, Garrett Morris talks with Wouter Swierstra and Niki Vazou about his work on Haskell’s type classes, how to fail successfully, and how to construct a set of ponies.

3 Likes
#2

@nomeata I’d suggest checking the related links. There seem to be quite a few typos:

Garrett’s

ditto

Rebekah

Data types à la carte

Jones’

1 Like
#3

Ah, that’s my bad. Fixing now!

1 Like
#4

This episode was great. I’m really looking forward to his work on defining the semantics of type classes on their own, not as translation to dictionary passing.

I also really enjoyed his paper on row types:

I hope we get something like that in Haskell one day.

1 Like
#5

Wow, yes, terrific talk! Thank you Wouter and Niki, and especially Garrett.

I’m pleased to hear someone is still talking about MPTCs and FunDeps and Overlapping Instances, and how they interact. GHC around a decade ago (there’s a slew of issues linked from that one) seemed to have just given up trying to bring the mess under some sort of control. I agree with Garrett we need a better ‘theory’ as a foundation to underpin Row types.

My attempt to specify how that should work. Note it’s going to reject some programs (sets of instances) that GHC currently accepts – but instances that you then might well find give incoherent type inference or mysterious rejections at usage sites. OTOH it accepts more programs than Hugs 2006 accepts; and I know that because I implemented that ‘theory’ in Hugs by relaxing a little of its overlaps validation.

Caveat: Hugs is an interpreter/doesn’t support separate compilation; so it looks at all instances to make sure they’re consistent together. GHC does support separate compilation; so there might be (overlapping) instances declared in other modules. I continue to think Instance Apartness Guards is the best fit approach for GHC; my thinking reinforced by implementing a rough mock-up in Hugs.

Having got that ‘theory’ working in Hugs, I could then implement a proper row algebra for TRex. To the example in the Intro to Morris & McKinna 2019:

∀ t z1 z2.(x ⊳ t) ⧁ (z1 ⊙ z2) ⇒ Πz1 → Πz2 → t.

Hugs infers:

(a\y, TrexApp b c (y :: d | a)) => Rec b -> Rec c -> d

where class TrexApp r1 r2 rr | r1 r2 -> rr, method trexApp :: Rec r1 -> Rec r2 -> Rec rr appends (>cough< merges) records r1, r2 providing they have no labels in common. (That restriction has to be expressed tediously on the instances.)

There’s a lot more meat in that 2019 paper; I’ll go through it in detail, thank you.

1 Like
#6

Most of the ‘related work’ in Garrett’s paper is from other functional languages/or which don’t have such a rich typeclass system as Haskell’s (especially not MPTCs, FunDeps, overlaps). Then the abstract approach sketched there is going to get messy …

I do have a real-world q on type classes and records (well, real-compiler) if anybody’s still listening. Consider this Hugs/Trex code:

--  auto-generated Eq instances for TRex

module TRexInstsEq  where

    import Hugs.Trex

{-  instance EqRecRow a => Eq (Rec a) where
      r == s = eqFields (eqRecRow r s)
               where eqFields = and . map snd

    -- constructor class with arity row
    class EqRecRow a where
      eqRecRow :: Rec a -> Rec a -> [(String,Bool)]
    instance EqRecRow EmptyRow where
      eqRecRow _ _ = []
-}

    xy = (x = 'x', y = True) == (y = False, x = 'x')
    
    xyz = (x = (), y = 'y', z = 3 :: Int) == (z = 4, y = 'Y', x = ())

For class Eq, Trex auto-generates the needed instances, which is a kindness. You need to import Hugs.Trex front-end module, which declares the linkage from class Eq to Trex-specific EqRecRow; and you get a base-case instance for EmptyRow.

Note different Trex rows might include the same label, but at different field types. The autogenerated instances really show the power of Trex, although they took me aback at first sight:

    instance (Eq a, b\x, EqRecRow b) => EqRecRow (x :: a | b)

    instance (Eq a, b\y, EqRecRow b) => EqRecRow (y :: a | b)

    instance (Eq a, b\z, EqRecRow b) => EqRecRow (z :: a | b)

IOW not a separate instance for each possible row type appearing in the program; merely an instance for each field-label (wherever it appears) polymorphic across all possible field types (providing Eq a).

  • The (x :: a | b) means a row including field labelled x at type a | with row tail b;
  • The constraint b\x means the tail b mustn’t include field x. IOW x appears uniquely in the overall row.

Now here’s my question: you can’t write instances in that style for yourself. Or rather to be more precise:

  • You can write one such manual instance for class EqRecRow, so the auto-gen’d ones must be ‘magic’/blessed; but
  • Any second instance gets rejected:
 Overlapping instances for class "EqRecRow"
*** This instance   : EqRecRow (v :: a | b)
*** Overlaps with   : EqRecRow (w :: a | b)
*** Common instance : EqRecRow (v :: a, w :: b | c)

Quite true: in (v :: a | b) it might be that the tail b includes field labelled w, and vice versa. But if that’s a restriction for my EqRecRow instances, why doesn’t it apply for the auto-gen’d?

This bites seriously when I want to write instances for my own class (say) row merging, or projecting one row on the labels appearing in another:

    class TrexProj r1 r2 rr  | r1 r2 -> rr  where
        trexProj :: Rec r1 -> Rec r2 -> Rec rr

    instance (r1'\x, r2'\x, TrexProj r1' ( x :: _b | r2') rr', rr'\x )            
             => TrexProj ( x :: a | r1') ( x :: _b | r2') ( x :: a | rr' )  where 
        trexProj ( x = x | r1') r2 = ( x = x | trexProj r1' r2 )

All credit to Trex: you can put rows in MPTCs and with FunDeps and it just works (for one instance) – including recursing along the row looking for matching field labels.

But any second instance gets rejected Overlapping instances .... I fersure aren’t going to write out a gazillion instances for each comb of whole-rows I want to Proj, Merge, Project-away (aka Remove).

So … I hacked Hugs’ instance overlap check:

  • If the instance header is of the form (x :: a | r) – that is, a single field plus row tail; and
  • the other instance’s (that is the one being checked for potential overlap) is of the same form but with a different field label; then
  • accept both instances together as really ‘apart’. (Or perhaps I mean really overlapping, but in a stable ordering. [**])
  • Note that Hugs’ instance selection operates after rows in terms have been normalised to the canonical ordering. But in any case for these purposes, the instances are dealing with one field/label at a time, each treatment orthogonal to the others.

[**] Hugs/Trex holds the ordering of field labels abstract. But you can see it’s alphabetical by field label. Never the less I don’t make any assumption about the ordering beyond it being stable within one compilationinterpreter run.

What I have is working for that highly stylised form of recursion (x :: a | b) in the instance head. If you’re going to get fancy with instance heads mentioning multiple labels and still wanting to recurse and/or multiple type params mentioning different labels, I imagine it’s going to quickly become incoherent. So it was valuable that Hugs out-of-the-box is much more disciplined than GHC with its instance overlap checks.

1 Like