Let's look at this example from a higher level.<br><br>Haskell is a language which allows you to write type signatures for functions, and even encourages you to do it.<br>Sometimes you even have to do it. Any language feature that stops me from writing a type signature is in my opinion broken.<br>
TFs as implemented in currently implemented ghc stops me from writing type signatures. They are thus, in my opinion, broken.<br><br>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.<br>
<br>To summarize: I don't care if the definition is useless, I want to be able to give it a type signature anyway.<br><br>(It's also pretty easy to fix the problem.)<br><br> -- Lennart<br><br><div class="gmail_quote">
On Wed, Apr 9, 2008 at 7:20 AM, Martin Sulzmann <<a href="mailto:martin.sulzmann@gmail.com">martin.sulzmann@gmail.com</a>> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Manuel said earlier that the source of the problem here is foo's ambiguous type signature<br>
(I'm switching back to the original, simplified example).<br>
Type checking with ambiguous type signatures is hard because the type checker has to guess<br>
types and this guessing step may lead to too many (ambiguous) choices. But this doesn't mean<br>
that this worst case scenario always happens.<br>
<br>
Consider your example again<div class="Ih2E3d"><br>
<br>
type family Id a<br>
<br>
type instance Id Int = Int<br>
<br></div>
foo :: Id a -> Id a<br>
foo = id<br>
<br>
foo' :: Id a -> Id a<br>
foo' = foo<br>
<br>
The type checking problem for foo' boils down to verifying the formula<br>
<br>
forall a. exists b. Id a ~ Id b<br>
<br>
Of course for any a we can pick b=a to make the type equation statement hold.<br>
Fairly easy here but the point is that the GHC type checker doesn't do any guessing<br>
at all. The only option you have (at the moment, there's still lots of room for improving<br>
GHC's type checking process) is to provide some hints, for example mimicking<br>
System F style type application by introducing a type proxy argument in combination<br>
with lexically scoped type variables.<br>
<br>
foo :: a -> Id a -> Id a<br>
foo _ = id<br>
<br>
foo' :: Id a -> Id a<br>
foo' = foo (undefined :: a)<br><font color="#888888">
<br>
<br>
Martin</font><div><div></div><div class="Wj3C7c"><br>
<br>
<br>
Ganesh Sittampalam wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
On Wed, 9 Apr 2008, Manuel M T Chakravarty wrote:<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
Sittampalam, Ganesh:<br>
</blockquote>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
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?<br>
</blockquote>
<br>
No, it is not know. Why do you think it is?<br>
</blockquote>
<br>
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?<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
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?<br>
</blockquote>
<br>
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).<br>
<br>
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.<br>
<br>
Cheers,<br>
<br>
Ganesh<br>
<br>
{-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances, NoMonomorphismRestriction #-}<br>
<br>
newtype Id a = Id { unId :: a }<br>
newtype Comp f g x = Comp { unComp :: f (g x) }<br>
<br>
type family Apply (f :: * -> *) a<br>
<br>
type instance Apply Id a = a<br>
type instance Apply (Comp f g) a = Apply f (Apply g a)<br>
type instance Apply SqlExpr a = SqlExpr a<br>
type instance Apply Maybe Int = Maybe Int<br>
type instance Apply Maybe Double = Maybe Double<br>
type instance Apply Maybe (Maybe a) = Apply Maybe a<br>
<br>
class DoubleToInt s where<br>
castNum :: Apply s Double -> Apply s Int<br>
<br>
instance DoubleToInt Id where<br>
castNum = round<br>
<br>
instance DoubleToInt SqlExpr where<br>
castNum = SECastNum<br>
<br>
data SqlExpr a where<br>
SECastNum :: SqlExpr Double -> SqlExpr Int<br>
<br>
castNum' :: (DoubleToInt s) => Apply s Double -> Apply s Int<br>
castNum' = castNum<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br>