[Haskell-cafe] Status of TypeDirectedNameResolution proposal?
simonpj at microsoft.com
Wed Nov 18 05:10:38 EST 2009
| 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
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.
More information about the Haskell-Cafe