[Haskell-cafe] Return of the revenge of the revisit of the extensible records, reiterated

[adam vogt]

On Wed, Nov 27, 2013 at 4:24 PM, AntC <anthony_clayden at clear.net.nz> wrote:
> The difficult part of extensible records is exactly avoiding duplicate
> labels. TRex achieved it, but needed costly language extensions.
> HList achieves it, using a fragile combination of extensions
> (and giving impenetrable type errors if your program gets it wrong).

Hi AntC,

Why do you say that errors regarding duplicate instances are impenetrable? They
are verbose, but the information you need is there if you ignore that "possible
fix" stuff. That is the same issue with type classes you may be familiar with in
haskell98. An example of that is what you get from: mean xs = sum xs / length xs
The HList type error looks like:

    No instance for (Fail * (DuplicatedLabel Symbol "x"))
      arising from a use of `.*.'
    Possible fix:
      add an instance declaration for
      (Fail * (DuplicatedLabel Symbol "x"))
    In the expression: x .=. 1 .*. x .=. 2 .*. emptyRecord
    In an equation for `r': r = x .=. 1 .*. x .=. 2 .*. emptyRecord

-- the file responsible:
{-# LANGUAGE DataKinds #-}
import Data.HList.CommonMain; import GHC.TypeLits
x = Label :: Label "x"
r = x .=. 1 .*. x .=. 2 .*. emptyRecord


> I think our best hope of building something workable
> is when Richard's overlapping/closed type functions gets into
> the language (and we probably have to allow time
> for the wrinkles to get ironed out).

Atze's code uses them. Failing when you insert
an element whose label already exists can be done
by adding another case in the `type family Inject'
(line 113 of OpenRecVar.hs) like:

  Inject l t (l := t ::: x) = Failure '("duplicated label", l)

This Failure is the same trick as done with Fail in HList
except translated to type families. Unfortunately the type
family Failure only shows up when you use the `x' below,
not when you define it (as happens in the previous example).

{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, UndecidableInstances #-}
import GHC.TypeLits

-- accepted, but not usable
x :: F Int Double
x = undefined

type family F a b where
    F a a = Bool
    F a b = Failure '("type",a, "should be equal to",b)

type family Failure (a :: k)

{- the "error" you get out of trying to use x is now something like:
    No instance for (Show
                       (Failure
                          ((,,,) Symbol * Symbol *)
                          '("type", Int, "should be equal to", Double)))

Or perhaps something like:
Expected type: (blah blah)
Actual type:   Failure ( ... )
-}

The same type error is also delayed if you make a
closed type family for Failure, which might be a ghc bug.
One promising idea is to make an infinite loop to bring
the error to attention earlier:

    Context reduction stack overflow; size = 201
    Use -fcontext-stack=N to increase stack size to N
      Fail
        ((,,,) Symbol * Symbol *)
        '("type", Int, "should be equal to", Double)
        (Fail
           Symbol
           "infinite loop to bring this to your attention: don't raise
the context stack please"
           t0)
      ~ a0
    In the expression: undefined
    In an equation for ‛x’: x = undefined

-- the above message comes from:
type family Fail (x::k) (a :: *) where
   Fail x a = Fail x (Fail "infinite loop to bring this to your
attention: don't raise the context stack please" a)

which gets used like:

    F a b = Fail '("type",a, "should be equal to",b) ()



Regards,
Adam