TDNR without new operators or syntax changes

[Dan Doel]

As a supplement, here's a series of definitions to think about. The
question is: what should happen in each section, and why? The more
detailed the answer, the better. Definitions from previous sections
are in scope in subsequent ones, for convenience. The examples are
arranged in a slippery slope, but there may be more good, confusing
examples that I missed.

--- cut ---

-- 1 --

f :: T -> Int
f t = ...

f :: U -> Int -> Char
f u = ...

t :: T
t = ...

u :: U
u = ...

i1 :: Int
i1 = f t

-- 2 --

g :: (T -> Int) -> Int
g h = h t

i2 :: Int
i2 = g f

-- 3 --

v :: T
v = t

v :: U
v = u

i3 :: Int
i3 = f v

-- 4 --

class C a where
  c :: a -> Int

instance C T where
  c = f

i4 :: Int
i4 = c v

-- 5 --

main = print $ f v

--- cut ---

-- Dan

On Tue, May 24, 2016 at 4:07 AM, Adam Gundry <adam at well-typed.com> wrote:
> Thanks for starting this discussion! Having spent more time thinking
> about record field overloading than perhaps I should, here are some
> things to think about...
>
>
> On 22/05/16 16:01, Jeremy wrote:
>> Bertram Felgenhauer-2 wrote
>>>> 1. If the compiler encounters a term f a, and there is more than one
>>>> definition for f in scope (after following all of the usual rules for
>>>> qualified imports);
>>>>
>>>> 2. And exactly one of these definitions matches the type of a (or the
>>>> expected type of f if given);
>>>>
>>>> 3. Then this is the definition to use.
>>>
>>> I now find that Anthony's concerns are justified. The question is, what
>>> exactly does the type matching in step 2 involve? If it is a recursive
>>> call to the type-checker then you'll have a huge performance problem.
>>
>> I was concerned about this, but not knowing anything about how
>> type-checking/inference is implemented, I wouldn't know if this is actually
>> a problem or not.
>
> Unfortunately this is indeed a problem. When the type-checker encounters
> `f a`, it infers the type of `f`, ensures it is a function type `s ->
> t`, then checks that `a` has type `s`. But if there are multiple
> possible `f`s in scope, what should it do? Options include:
>
>  1. run the entire type-checking process for each possible type of `f`
> (this is almost certainly too slow);
>
>  2. give ad-hoc rules to look at type information from the context or
> the inferred type of the argument `a`;
>
>  3. introduce a name resolution constraint and defer it to the
> constraint solver (the same way that solving for typeclasses works);
>
>  4. require a type signature in a fixed location.
>
> Both 2 and 3 would need careful specification, as they run the risk of
> exposing the type-checking algorithm to the user, and changing the
> typing rules depending on what is in scope may be problematic. In
> particular, if `f` has a higher-rank type than bidirectional type
> inference is likely to break down.
>
> The DuplicateRecordFields approach is to make use of bidirectional type
> inference (a bit like 2, but without looking at the type of the
> argument) and otherwise require a type signature. This is carefully
> crafted to avoid needing to change existing typing rules. The wiki page
> [1] sets out some of the cases in which this does and doesn't work.
>
> Point 3 is rather like the magic classes in the OverloadedRecordFields
> proposal [2] (this isn't in GHC HEAD yet, but an early version is on
> Phab [3]).
>
>
>>> If, on the other hand, you only take into account what is known about
>>> the type of a at a given time, then you need special treatment for
>>> unambiguous names or even trivial programs will fail to type-check, just
>>> as Anthony said.
>>
>> Why special treatment for unambiguous names? They shouldn't be effected at
>> all by this.
>
> There are some design choices here as well, separately from the options
> above. Some possibilities are:
>
>  A. leave unambiguous names alone, and only do the special thing for the
> ambiguous ones (this doesn't break existing code, but can lead to
> confusing errors if an import is changed to introduce or remove an
> ambiguity, especially for options 2 or 3 above);
>
>  B. do the same thing for unambiguous names as ambiguous ones (but this
> may well break existing code, and is likely to restrict inference too much);
>
>  C. require an explicit syntactic cue that the name should be treated
> specially (e.g. the original TDNR's use of dot, or the # sign in the
> OverloadedLabels part of ORF [4]).
>
>
> As you can see, there are quite a few complex trade-offs here. I suspect
> this is at least part of the reason for the slow progress on TDNR-like
> extensions. It will be interesting to see how DuplicateRecordFields is
> received!
>
> All the best,
>
> Adam
>
>
> [1]
> https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/DuplicateRecordFields
>
> [2]
> https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/MagicClasses
>
> [3] https://phabricator.haskell.org/D1687
>
> [4]
> https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/OverloadedLabels
>
>
> --
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users