| 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
