[Haskell-cafe] Status of TypeDirectedNameResolution proposal?

[Simon Peyton-Jones]

| Simon, have you given any thought to how this interacts with type system
| extensions, in particular with GADTs and type families? The proposal relies
| on being able to "find the type" of a term but it's not entirely clear to me
| what that means. Here is an example:
| 
| foo :: F Int -> Int
| foo :: Int -> Int
| 
| bar1 :: Int -> Int
| bar1 = foo
| 
| bar2 :: Int ~ F Int => Int -> Int
| bar2 = foo
| 
| IIUC, bar1 is ok but bar2 isn't. Do we realy want to have such a strong
| dependency between name lookup and type inference? Can name lookup be
| specified properly without also having to specify the entire inference
| algorithm?

Yes I think it can, although you are right to point out that I said nothing about type inference.  One minor thing is that you've misunderstood the proposal a bit.  It ONLY springs into action when there's a dot.  So you'd have to write
	bar1 x = x.foo
	bar2 x = x.foo

OK so now it works rather like type functions.  Suppose, the types with which foo was in scope were
	foo :: Int -> Int
	foo :: Bool -> Char

Now imagine that we had a weird kind of type function

	type instance TDNR_foo Int = Int -> Int
	type instance TDNR_foo Bool = Bool -> Char

Each 'foo' gives a type instance for TDNR_foo, mapping the type of the first argument to the type of that foo.

So when we see (x.foo) we produce the following constraints

	TDNR_foo tx ~ tx -> tr

where x:tx and the result type is tr.  Then we can solve at our leisure. We can't make progress until we know 'tx', but when we do we can choose which foo is used.  Of course, there'd be some modest built-in machinery rather than a forest of 


Now you rightly ask what if
	foo :: F Int -> Int

Now under my "type function" analogy, we'd get
	type instance TDNR_foo (F Int) = F Int -> Int
and now we may be in trouble because type functions can't have a type function call in an argument pattern.

I hadn't thought of that.  The obvious thing to do is to *refrain* from adding a "type instance" for such a 'foo'.  But that would be a bit odd, because it would silently mean that some 'foo's (the ones whose first argument involved type functions) just didn't participate in TDNR at all.  But we can hardly emit a warning message for every function with a type function in the first argument!

I suppose that if you use x.foo, we could warn if any in-scope foo's have this property, saying "you might have meant one of these, but I can't even consider them".  


GADTs, on the other hand, are no problem.


| Another example: suppose we have
| 
| data T a where
|   TInt  :: T Int
|   TBool :: T Bool
| 
| foo :: T Int -> u
| foo :: T Bool -> u
| 
| bar :: T a -> u
| bar x = case x of
| 	  TInt  -> foo x
| 	  TBool -> foo x
| 
| Here, (foo x) calls different functions in the two alternatives, right? To be
| honest, that's not something I'd like to see in Haskell.

You mean x.foo and x.foo, right?  Then yes, certainly. 

Of course that's already true of type classes:

	data T a where
         T1 :: Show a => T a
	  T2 :: Sow a => T a

       bar :: a -> T a -> String
       bar x y = case y of
                   T1 -> show x
                   T2 -> show x

Then I get different show's.

Simon