[Haskell-cafe] Type Directed Name Resolution

[Dan Doel]

On Wednesday 10 November 2010 2:08:56 pm Lauri Alanko wrote:
> So the proposal seems to be tailored specifically to fix some
> inconveniences with records. I'd much rather see a true record system
> for Haskell, since that would fix the namespace conflict problem in a
> more robust way.

I certainly agree with this.

> Plain ad hoc overloading might or might not be a sensible addition to
> Haskell, but please at least drop the "x .f" syntax, it's a pointless
> hack that makes the lexical status of "." even more difficult than it
> currently is. After all, one can simply define e.g. "x .$ f = f x" if
> postfix application is needed.

However, I don't completely agree with this. I agree with '.' perhaps not 
being a good choice. However, if we do add completely ad-hoc overloading, I 
think it might be useful to give functions subject to it a different syntactic 
appearance, to alert to where it is being used.

----------

For a case study, Agda has type directed name resolution, but *only* for 
constructors. If you try to define something else with the same name as a 
constructor, or define two other values with the same name, it will reject 
your program. This can be useful, since you can write:

  _+N_ : Nat -> Nat -> Nat
  zero  +N n = n
  suc m +N n = suc (m +N n)

  _+F_ : forall {i j} -> Fin i -> Fin j -> Fin (i +N j)
  zero  +F n = n
  suc m +F n = suc (m +F n)

But, it has two caveats, I think:

1) It seems significantly less of a burden due to the fact that Agda requires 
you to write signatures for *every* function you write already.

2) Even with just the constructor case, enough ambiguity is introduced that 
the Agda implementors recently added the ability to qualify a constructor by 
its associated datatype. For instance, the signature:

  foo : forall n -> n /= suc n

is ambiguous, since n has no principal type. You could fix this via:

  foo : forall (n : Nat) -> n /= suc n

but there is now also support to write:

  foo : forall n -> n /= Nat.suc n

I'll admit, the Agda overloading is handy. But I've always considered 
Haskell's lack of ad-hoc overloading to be a feature. Type classes give 
sensible types for what would normally be ad-hoc. Adding back ad-hoc functions 
that have no available general type feels like a step backward. Perhaps that's 
just me, though.

-- Dan