[Haskell-cafe] Status of TypeDirectedNameResolution proposal?

[Roman Leshchinskiy]

On 18/11/2009, at 21:10, Simon Peyton-Jones wrote:

> 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

Yes, that's what I meant to write, silly me. I promise to pay more attention next time.

> 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.

Hmm... GHC doesn't allow this:

type instance TDNR_foo () = forall a. () -> a -> a

IIUC this restriction is necessary to guarantee termination. Given your analogy, wouldn't this proposal run into similar problems?

> | 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.

How so? Surely you'll get the same Show instance in both cases unless you have conflicting instances in your program?

Roman