I think it's not fair to say TFs as implemented in GHC are broken.
Fine, they are situations where the current implementation is overly
conservative.
The point is that the GHC type checker relies on automatic inference.
Hence, there'll
always be cases where certain "reasonable" type signatures are rejected.
For example, consider the case of "undecidable" and "non-confluent" type
class instances.
instance Foo a => Bar a -- (1)
instance Erk a => Bar [a] -- (2)
GHC won't accept the above type class instance (note: instances are a
kind of type signature) because
- instance (1) is potentially non-terminating (the size of the type term
is not decreasing)
- instance (2) overlaps with (1), hence, it can happen that during
context reduction we choose
the "wrong" instance.
To conclude, any system with automatic inference will necessary reject
certain type signatures/instances
in order to guarantee soundness, completeness and termination.
Lennart, you said
(It's also pretty easy to fix the problem.)
What do you mean? Easy to fix the type checker, or easy to fix the
program by inserting annotations
to guide the type checker?
Martin
Lennart Augustsson wrote:
Let's look at this example from a higher level.
Haskell is a language which allows you to write type signatures for
functions, and even encourages you to do it.
Sometimes you even have to do it. Any language feature that stops me
from writing a type signature is in my opinion broken.
TFs as implemented in currently implemented ghc stops me from writing
type signatures. They are thus, in my opinion, broken.
A definition should either be illegal or it should be able to have a
signature. I think this is a design goal. It wasn't true in Haskell
98, and it's generally agreed that this was a mistake.
To summarize: I don't care if the definition is useless, I want to be
able to give it a type signature anyway.
(It's also pretty easy to fix the problem.)
-- Lennart
On Wed, Apr 9, 2008 at 7:20 AM, Martin Sulzmann
<[EMAIL PROTECTED] <mailto:[EMAIL PROTECTED]>> wrote:
Manuel said earlier that the source of the problem here is foo's
ambiguous type signature
(I'm switching back to the original, simplified example).
Type checking with ambiguous type signatures is hard because the
type checker has to guess
types and this guessing step may lead to too many (ambiguous)
choices. But this doesn't mean
that this worst case scenario always happens.
Consider your example again
type family Id a
type instance Id Int = Int
foo :: Id a -> Id a
foo = id
foo' :: Id a -> Id a
foo' = foo
The type checking problem for foo' boils down to verifying the formula
forall a. exists b. Id a ~ Id b
Of course for any a we can pick b=a to make the type equation
statement hold.
Fairly easy here but the point is that the GHC type checker
doesn't do any guessing
at all. The only option you have (at the moment, there's still
lots of room for improving
GHC's type checking process) is to provide some hints, for example
mimicking
System F style type application by introducing a type proxy
argument in combination
with lexically scoped type variables.
foo :: a -> Id a -> Id a
foo _ = id
foo' :: Id a -> Id a
foo' = foo (undefined :: a)
Martin
Ganesh Sittampalam wrote:
On Wed, 9 Apr 2008, Manuel M T Chakravarty wrote:
Sittampalam, Ganesh:
No, I meant can't it derive that equality when
matching (Id a) against (Id b)? As you say, it can't
derive (a ~ b) at that point, but (Id a ~ Id b) is
known, surely?
No, it is not know. Why do you think it is?
Well, if the types of foo and foo' were forall a . a -> a and
forall b . b -> b, I would expect the type-checker to unify a
and b in the argument position and then discover that this
equality made the result position unify too. So why can't the
same happen but with Id a and Id b instead?
The problem is really with foo and its signature, not with
any use of foo. The function foo is (due to its type)
unusable. Can't you change foo?
Here's a cut-down version of my real code. The type family
Apply is very important because it allows me to write class
instances for things that might be its first parameter, like
Id and Comp SqlExpr Maybe, without paying the syntactic
overhead of forcing client code to use Id/unId and
Comp/unComp. It also squishes nested Maybes which is important
to my application (since SQL doesn't have them).
castNum is the simplest example of a general problem - the
whole point is to allow clients to write code that is
overloaded over the first parameter to Apply using primitives
like castNum. I'm not really sure how I could get away from
the ambiguity problem, given that desire.
Cheers,
Ganesh
{-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances,
NoMonomorphismRestriction #-}
newtype Id a = Id { unId :: a }
newtype Comp f g x = Comp { unComp :: f (g x) }
type family Apply (f :: * -> *) a
type instance Apply Id a = a
type instance Apply (Comp f g) a = Apply f (Apply g a)
type instance Apply SqlExpr a = SqlExpr a
type instance Apply Maybe Int = Maybe Int
type instance Apply Maybe Double = Maybe Double
type instance Apply Maybe (Maybe a) = Apply Maybe a
class DoubleToInt s where
castNum :: Apply s Double -> Apply s Int
instance DoubleToInt Id where
castNum = round
instance DoubleToInt SqlExpr where
castNum = SECastNum
data SqlExpr a where
SECastNum :: SqlExpr Double -> SqlExpr Int
castNum' :: (DoubleToInt s) => Apply s Double -> Apply s Int
castNum' = castNum
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org <mailto:Haskell-Cafe@haskell.org>
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org <mailto:Haskell-Cafe@haskell.org>
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
