Re: [Haskell-cafe] type families and type signatures
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
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] type families and type signatures
OK, thanks. I think I'm finally understanding :-)
Cheers,
Ganesh
-Original Message-
From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of Martin Sulzmann
Sent: 09 April 2008 07:21
To: Ganesh Sittampalam
Cc: Manuel M T Chakravarty; haskell-cafe@haskell.org
Subject: Re: [Haskell-cafe] type families and type signatures
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
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
==
Please access the attached hyperlink for an important electronic communications
disclaimer:
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
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]
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
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
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
Re: [Haskell-cafe] type families and type signatures
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
Re: [Haskell-cafe] type families and type signatures
Claus Reinke wrote: type family Id a type instance Id Int = Int foo :: Id a - Id a foo = id n foo' :: Id a - Id a foo' = foo type function notation is slightly misleading, as it presents qualified polymorphic types in a form usually reserved for unqualified polymorphic types. rewriting foo's type helped me to see the ambiguity that others have pointed out: foo :: r ~ Id a = r - r there's nowhere to get the 'a' from. so unless 'Id' itself is fully polymorphic in 'a' (Id a = a, Id a = Int, ..), 'foo' can't really be used. for each type variable, there needs to be at least one position where it is not used as a type family parameter. Correct because type family constructors are injective only. [Side note: With FDs you can enforce bijection class Inj a b | a - b class Bij a b | a - b, b - a ] it might be useful to issue an ambiguity warning for such types? perhaps, with closed type families, one might be able to reason backwards (is there a unique 'a' such that 'Id a ~ Int'?), as with bidirectional FDs. but if you want to flatten all 'Maybe'-nests, even that direction isn't unique. True, type checking with closed type families will rely on some form of solving and then we're more likely to guess (the right) types. The type checking problem for foo' boils down to verifying the formula forall a. exists b. Id a ~ Id b naively, i'd have expected to run into this instead/first: (forall a. Id a - Id a) ~ (forall b. Id b - Id b) which ought to be true modulo alpha conversion, without guesses, making 'foo'' as valid/useless as 'foo' itself. where am i going wrong? You're notion of subsumption is too strong here. I've been using (forall as. C = t) = (forall bs. C' = t') iff forall bs. (C' implies exist bs. (C /\ t=t')) where (forall as. C = t) is the inferred type (forall bs. C' = t') is the annotated type Makes sense? Even if we establish (forall a. Id a - Id a) ~ (forall b. Id b - Id b) we'd need to guess a ~ b (which is of course obvious) claus ps. i find these examples and discussions helpful, if often initially puzzling - they help to clear up weak spots in the practice of type family use, understanding, and implementation, thereby improving all while making families more familiar!-) Absolutely! Martin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
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. .. To conclude, any system with automatic inference will necessary reject certain type signatures/instances in order to guarantee soundness, completeness and termination. i think Lennart's complaint is mainly about cases where GHC does not accept the very type signature it infers itself. all of which cases i'd consider bugs myself, independent of what type system feature they are related to. there are also the related cases of type signatures which cannot be expressed in the language but which might occur behind the scenes. all of these cases i'd consider language limitations that ought to be removed. the latter cases also mean that type errors are reported either in a syntax that can not be used in programs or in a misleading external syntax that does not fully represent the internal type. in this example, ghci infers a type for foo' that it rejects as a type signature for foo'. so, either the inferred type is inaccurately presented, or there's a gap in the type system, between inferred and declared types, right? claus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: type families and type signatures
However, I have this feeling that bar :: forall a . Id a - String with a type family Id *is* parametric in the sense that no matter what a is, the result always has to be the same. Intuitively, that's because we may not pattern match on the branch of a definition like type instance Id String = .. type instance Id Int= .. .. But in a degenerate case there could be just this one instance: type instance Id x = GADT x which then reduces this example to the GADT case of which you said that is was clearly parametric. Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: [EMAIL PROTECTED] url: http://www.cs.kuleuven.be/~toms/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance Monad m = Functor m
On 9 Apr 2008, at 11:26, Jules Bean wrote: Using 'hugs -98', I noticed it accepts: instance Monad m = Functor m where fmap f x = x = return.f Has this been considered (say) as a part of the upcoming Haskell Prime? This forbids any Functors which are not monads. Unless you allow overlapping instances... I see it as a Haskell limitation of not being able to indicate the function names in the class definition head: If one could write say class Monoid (a; unit, mult) where unit :: a mult :: a - a - a then it is possible to say instance Monoid ([]; [], (++)) where -- 'unit' already defined -- definition of (++) Similarly: class Functor (m; fmap) where fmap :: (a - b) - (m a - m b) instance Monad m = Functor (m, mmap) where mmap f x = x = return.f - For backwards compatibility, if the function names are not indicated, one gets the declaration names as default. I don't know if it is possible to extend the syntax this way, but it would be closer to math usage. And one would avoid duplicate definitions just to indicate different operator names, like: class AdditiveMonoid a where o :: a (+) :: a - a - a as it could be create using class Monoid (a; o, (+)) ...(which of course would not be h98 any more!). It does not work in 'hugs +98' mode; if I avoid the Prelude names by: class Munctor m where mmap :: (a - b) - (m a - m b) instance Monad m = Munctor m where mmap f x = x = return.f I get ERROR - Syntax error in instance head (constructor expected) Other solutions, such as class Functor m = Monad m are frequently discussed. The point is that Monads have a code lifting property, so the functor is already conatained in the current definition. One might want to have away to override, so even if instance Monad m = Functor (m, mmap) functor specialization can take place if one has a more efficeint definition. For example instance Functor ([], mmap) where mmap = map Hans ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: type families and type signatures
Manuel M T Chakravarty wrote: apfelmus: Manuel M T Chakravarty wrote: Let's alpha-rename the signatures and use explicit foralls for clarity: foo :: forall a. Id a - Id a foo' :: forall b. Id b - Id b GHC will try to match (Id a) against (Id b). As Id is a type synonym family, it would *not* be valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.) While in general (Id a ~ Id b) -/- (a ~ b) , parametricity makes it true in the case of foo . For instance, let Id a ~ Int . Then, the signature specializes to foo :: Int - Int . But due to parametricity, foo does not care at all what a is and will be the very same function for every a with Id a ~ Int . In other words, it's as if the type variable a is not in scope in the definition of foo . Be careful, Id is a type-indexed type family and *not* a parametric type. Parametricity does not apply. For more details about the situation with GADTs alone, see Foundations for Structured Programming with GADTs. Patricia Johann and Neil Ghani. Proceedings, Principles of Programming Languages 2008 (POPL'08). Yes and no. In the GADT case, a function like bar :: forall a . GADT a - String is clearly not parametric in a, in the sense that pattern matching on the GADT can specialize a which means that we have some form of pattern matching on the type a . The resulting String may depend on the type a . So, by parametricity, I mean type arguments may not be inspected. Likewise, bar :: forall a . Show a = Phantom a - String is not parametric in a since the result may depend on the type a . However, I have this feeling that bar :: forall a . Id a - String with a type family Id *is* parametric in the sense that no matter what a is, the result always has to be the same. Intuitively, that's because we may not pattern match on the branch of a definition like type instance Id String = .. type instance Id Int= .. .. So, in the special case of foo and foo' , solving Id b ~ Id a by guessing a ~ b is safe since foo is parametric in a . Every guess is fine. I don't think that this can be squeezed into a type inference/checking algorithm, though. In full System F , neither definition would be a problem since the type a is an explicit parameter. You can't generally translate type family/GADT programs into System F. We proposed an extension of System F called System F_C(X); see our TLDI'07 paper: http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html Yes of course. I just wanted to remark that the whole ambiguity stuff is only there because we don't (want to) have explicit type application à la System F(_C(X)). Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Claus Reinke wrote: 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. .. To conclude, any system with automatic inference will necessary reject certain type signatures/instances in order to guarantee soundness, completeness and termination. i think Lennart's complaint is mainly about cases where GHC does not accept the very type signature it infers itself. all of which cases i'd consider bugs myself, independent of what type system feature they are related to. there are also the related cases of type signatures which cannot be expressed in the language but which might occur behind the scenes. all of these cases i'd consider language limitations that ought to be removed. the latter cases also mean that type errors are reported either in a syntax that can not be used in programs or in a misleading external syntax that does not fully represent the internal type. in this example, ghci infers a type for foo' that it rejects as a type signature for foo'. so, either the inferred type is inaccurately presented, or there's a gap in the type system, between inferred and declared types, right? Good point(s) which I missed earlier. Type inference (no annotations) is easy but type checking is much harder. Type checking is not all about pure checking, we also perform some inference, the Hindley/Milner unification variables which arise out of the program text (we need to satisfy these constraints via the annotation). To make type checking easier we should impose restrictions on inference. We (Tom/SimonPJ/Manuel) thought about this possibility. The problem is that it's hard to give an intuitive, declarative description of those restrictions. Martin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance Monad m = Functor m
Hans Aberg wrote: Using 'hugs -98', I noticed it accepts: instance Monad m = Functor m where fmap f x = x = return.f Has this been considered (say) as a part of the upcoming Haskell Prime? This forbids any Functors which are not monads. Unless you allow overlapping instances (which of course would not be h98 any more!). Other solutions, such as class Functor m = Monad m are frequently discussed. I see no H' ticket for it, though. Jules ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
type family Id a type instance Id Int = Int foo :: Id a - Id a foo = id n foo' :: Id a - Id a foo' = foo type function notation is slightly misleading, as it presents qualified polymorphic types in a form usually reserved for unqualified polymorphic types. rewriting foo's type helped me to see the ambiguity that others have pointed out: foo :: r ~ Id a = r - r there's nowhere to get the 'a' from. so unless 'Id' itself is fully polymorphic in 'a' (Id a = a, Id a = Int, ..), 'foo' can't really be used. for each type variable, there needs to be at least one position where it is not used as a type family parameter. it might be useful to issue an ambiguity warning for such types? perhaps, with closed type families, one might be able to reason backwards (is there a unique 'a' such that 'Id a ~ Int'?), as with bidirectional FDs. but if you want to flatten all 'Maybe'-nests, even that direction isn't unique. The type checking problem for foo' boils down to verifying the formula forall a. exists b. Id a ~ Id b naively, i'd have expected to run into this instead/first: (forall a. Id a - Id a) ~ (forall b. Id b - Id b) which ought to be true modulo alpha conversion, without guesses, making 'foo'' as valid/useless as 'foo' itself. where am i going wrong? claus ps. i find these examples and discussions helpful, if often initially puzzling - they help to clear up weak spots in the practice of type family use, understanding, and implementation, thereby improving all while making families more familiar!-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance Monad m = Functor m
On Wed, 9 Apr 2008, Hans Aberg wrote: I don't know if it is possible to extend the syntax this way, but it would be closer to math usage. And one would avoid duplicate definitions just to indicate different operator names, like: class AdditiveMonoid a where o :: a (+) :: a - a - a as it could be create using class Monoid (a; o, (+)) I also recognized that problem in the past, but didn't know how to solve it. In Haskell 98, methods are resolved using the types of the operands. How would the compiler find out which implementation of (+) to choose for an expression like x+y using your approach? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Lock-Free Data Structures using STMs in Haskell
I recently read the STM paper on lock-free data structures [1] which I
found very informative in my quest to learn how to use STM. However,
there are a few things I do not fully understand and was hoping
someone might be able to explain further.
In the STM version of the ArrayBlockingQueue, the following type is
defined:
data ArrayBlockingQueueSTM e = ArrayBlockingQueueSTM {
shead :: TVar Int,
stail :: TVar Int,
sused :: TVar Int,
slen :: Int,
sa :: Array Int (TVar e)
}
It's unclear to me why the Array's elements must be wrapped in TVars.
Why aren't the TVars on shead, stail, and sused sufficient? Here is
the only function that reads from the queue:
readHeadElementSTM :: ArrayBlockingQueueSTM e
- Bool - Bool - STM (Maybe e)
readHeadElementSTM abq remove block
= do u - readTVar (sused abq)
if u == 0
then if block
then retry
else return Nothing
else do h - readTVar (ihead abq)
let tv = sa abq ! h
-- Why are the array elements wrapped in TVars?
e - readTVar tv
if remove
then do
let len = slen abq
let newh = h `mod` len
writeTVar (shead abq) $! newh
writeTVar (sused abq) $! (u-1)
else return ()
return (Just e)
It is not immediately obvious to me why the elements need to be
wrapped in TVars. Could someone help elaborate?
The other question is in regards to section 2 where STM is
introduced. The authors define the following:
decT :: TVar Int - IO ()
decT v = atomically (do x - readTVar v
if x == 0
then retry
else return ()
writeTVar v (x-1))
And then go on to show how easy it is to compose STM types with this
function:
decPair v1 v1 :: TVar Int - TVar Int - IO ()
decPair v1 v2 = atomically (decT v1 `orElse` decT v2)
Will this actually compile? I was under the impression that 'orElse'
could only combine STM types, not IO () types.
Thank you,
Pete
[1] Anthony Discolo, Tim Harris, Simon Marlow, Simon Peyton Jones, and
Satnam Singh. Lock-free data structures using STMs in Haskell. In
Eighth International Symposium on Functional and Logic Programming
(FLOPS.06), April 2006.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance Monad m = Functor m
On 9 Apr 2008, at 15:23, Henning Thielemann wrote: I don't know if it is possible to extend the syntax this way, but it would be closer to math usage. And one would avoid duplicate definitions just to indicate different operator names, like: class AdditiveMonoid a where o :: a (+) :: a - a - a as it could be create using class Monoid (a; o, (+)) I also recognized that problem in the past, but didn't know how to solve it. In Haskell 98, methods are resolved using the types of the operands. How would the compiler find out which implementation of (+) to choose for an expression like x+y using your approach? Different names result in different operator hierarchies. So a class like class Monoid (a; unit, mult) where unit :: a mult :: a - a - a must have an instantiation that specifies the names of the operators. In particular, one will need a class (Monoid (a; 0; (+)), ...) = Num a ... if (+) should be used as Monoid.(+) together with Num.(+). Or give an example you think may cause problems, and I will give it a try. Hans ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance Monad m = Functor m
On Wed, 9 Apr 2008, Hans Aberg wrote: Different names result in different operator hierarchies. So a class like class Monoid (a; unit, mult) where unit :: a mult :: a - a - a must have an instantiation that specifies the names of the operators. In particular, one will need a class (Monoid (a; 0; (+)), ...) = Num a ... if (+) should be used as Monoid.(+) together with Num.(+). Or give an example you think may cause problems, and I will give it a try. I think a classical example are number sequences which can be considered as rings in two ways: 1. elementwise multiplication 2. convolution and you have some function which invokes the ring multiplication f :: Ring a = a - a and a concrete sequence x :: Sequence Integer what multiplication (elementwise or convolution) shall be used for computing (f x) ? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance Monad m = Functor m
On 9 Apr 2008, at 15:23, Henning Thielemann wrote: I also recognized that problem in the past, but didn't know how to solve it. In Haskell 98, methods are resolved using the types of the operands. How would the compiler find out which implementation of (+) to choose for an expression like x+y using your approach? I might describe the idea via mangling. So if one has class Magma (a; unit, mult) where unit :: a mult :: a - a - a then instances Monoid (a; 0; (+)) Monoid (a; 1; (*)) should logically equivalent to Monoid_0_+ (a) 0 :: a (+) :: a - a - a Monoid_1_* (a) 1 :: a (*) :: a - a - a or whatever internal mangling that ensures that the names Monoid_0_+ and Monoid_1_* are different. Would this not work? - They code should be essentially a shortcut for defining new classes. Hans ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance Monad m = Functor m
On 9 Apr 2008, at 16:26, Henning Thielemann wrote: I think a classical example are number sequences which can be considered as rings in two ways: 1. elementwise multiplication 2. convolution and you have some function which invokes the ring multiplication f :: Ring a = a - a and a concrete sequence x :: Sequence Integer what multiplication (elementwise or convolution) shall be used for computing (f x) ? For that problem to arise, one must have, when defining Sequence class Ring (a; o, e, add, mult) ... class (Ring(a; o, e, add, (*)), Ring(a; o, e, add, (**)) = Sequence a It is a good question, but can be avoided by not admitting such constructs. - I will think a bit more on it. Hans ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance Monad m = Functor m
On 9 Apr 2008, at 16:26, Henning Thielemann wrote: 1. elementwise multiplication 2. convolution and you have some function which invokes the ring multiplication f :: Ring a = a - a and a concrete sequence x :: Sequence Integer what multiplication (elementwise or convolution) shall be used for computing (f x) ? In math, if there is a theorem about a ring, and one wants to apply it to an object which more than one ring structure, one needs to indicate which ring to use. So if I translate, then one might get something like class Ring (a; o, e, add, mult) ... ... class Ring(a; o, e, add, (*)) = Sequence.mult a Ring(a; o, e, add, (**) = Sequence.conv a where ... Then Sequence.mult and Sequence.conv will be treated as different types whenever there is a clash using Sequence only. - I am not sure how this fits into Haskell syntax though. This might be useful, if it can be worked out. Hans ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance Monad m = Functor m
On Wed, 9 Apr 2008, Hans Aberg wrote: On 9 Apr 2008, at 16:26, Henning Thielemann wrote: 1. elementwise multiplication 2. convolution and you have some function which invokes the ring multiplication f :: Ring a = a - a and a concrete sequence x :: Sequence Integer what multiplication (elementwise or convolution) shall be used for computing (f x) ? In math, if there is a theorem about a ring, and one wants to apply it to an object which more than one ring structure, one needs to indicate which ring to use. So if I translate, then one might get something like class Ring (a; o, e, add, mult) ... ... class Ring(a; o, e, add, (*)) = Sequence.mult a Ring(a; o, e, add, (**) = Sequence.conv a where ... Then Sequence.mult and Sequence.conv will be treated as different types whenever there is a clash using Sequence only. - I am not sure how this fits into Haskell syntax though. Additionally I see the problem, that we put more interpretation into standard symbols by convention. Programming is not only about the most general formulation of an algorithm but also about error detection. E.g. you cannot compare complex numbers in a natural way, that is x (y :: Complex Rational) is probably a programming error. However, some people might be happy if () is defined by lexicgraphic ordering. This way complex numbers can be used as keys in a Data.Map. But then accidental uses of () could no longer be detected. (Thus I voted for a different class for keys to be used in Data.Map, Data.Set et.al.) Also (2*5 == 7) would surprise people, if (*) is the symbol for a general group operation, and we want to use it for the additive group of integers. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance Monad m = Functor m
On 9 Apr 2008, at 17:49, Henning Thielemann wrote: Additionally I see the problem, that we put more interpretation into standard symbols by convention. Programming is not only about the most general formulation of an algorithm but also about error detection. E.g. you cannot compare complex numbers in a natural way, that is x (y :: Complex Rational) is probably a programming error. However, some people might be happy if () is defined by lexicgraphic ordering. This way complex numbers can be used as keys in a Data.Map. But then accidental uses of () could no longer be detected. (Thus I voted for a different class for keys to be used in Data.Map, Data.Set et.al.) I think there it might be convenient with a total order defined on all types, for that data-map sorting purpose you indicate. But it would then be different from the semantic order that some types have. So the former should have a different name. Also, one might have Ordering(LT, EQ, GT, Unrelated) so t can be used on all relations. Also (2*5 == 7) would surprise people, if (*) is the symbol for a general group operation, and we want to use it for the additive group of integers. This is in fact as it should be; the idea is to admit such things: class Group(a; unit, inverse, mult) ... class (Group(a; 0, (-), (+)), Monoid(a; 1, (*)) = Ring(a; 0, 1, (-), (+), (*)) ... -- (or better variable names). instance Ring(a; 0, 1, (-), (+), (*)) = Integer A group can be written additively or multiplicatively, (+) is often reserved for commutative operations. But there is not way to express that, unless one can write class AbelianGroup(a; unit, inverse, mult) where ... satisfying mult a b = mult b a One would need pattern matching to Haskell in order to make this useful. Hans ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann [EMAIL PROTECTED] wrote: 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 I'm referring to the situation where the type inferred by the type checker is illegal for me to put into the program. In our example we can fix this in two ways, by making foo' illegal even when it has no signature, or making foo' legal even when it has a signature. To make it illegal: If foo' has no type signature, infer a type for foo', insert this type as a signature and type check again. If this fails, foo' is illegal. To make it legal: If foo' with a type signature doesn't type check, try to infer a type without a signature. If this succeeds then check that the type that was inferred is alpha-convertible to the original signature. If it is, accept foo'; the signature doesn't add any information. Either of these two option would be much preferable to the current (broken) situation where the inferred signature is illegal. -- Lennart ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance Monad m = Functor m
On 9 Apr 2008, at 17:49, Henning Thielemann wrote: Also (2*5 == 7) would surprise people, if (*) is the symbol for a general group operation, and we want to use it for the additive group of integers. One might resolve the Num binding of (+) problem by putting all operators into an implicit superclass: Roughly, let T be the set of of most general types, and for each t in T define a mangling string s(t). Then if the operator op :: t is defined somewhere, it is internally defined as class Operator_s(t)_op t where op :: t Then usages of it get implicit class (Operator_s(t)_op t, ...) = Class where ... and instance Operator_s(t)_op t where ... If I now have another class using (+), it need not be derived from Num, as both usages are derivable from an internal class Operator_(+) The mangling of the type via s(t) might be used to generate C++ style name overloading. It will then depend on how much ambiguity one wants to accept in the context. I do not see exactly how this works with Haskell current syntax; just an input. Hans ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lock-Free Data Structures using STMs in Haskell
decPair v1 v1 :: TVar Int - TVar Int - IO () decPair v1 v2 = atomically (decT v1 `orElse` decT v2) Will this actually compile? I was under the impression that 'orElse' could only combine STM types, not IO () types. The type of atomically is STM a - IO a. But orElse :: STM a - STM a - STM a decT can be of type TVar Int - STM () if you leave out the atomically. -- Ariel J. Birnbaum ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What's the difference?
For me, the word implies is too tied in my brain to an arrow symbol to be useful to me in keeping the implications straight. Pun implied? -- Ariel J. Birnbaum ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] problems building hpodder
On Tue, 2008-04-08 at 15:43 -0500, John Goerzen wrote: On Tue April 8 2008 3:21:34 pm Karl Hasselström wrote: http://www.haskell.org/haskellwiki/Package_versioning_policy seems to have something relevant to say. build-depends: HaXml = 1.13.3 1.14 ought to do the trick, since any changes in the published interface are supposed to be accompanied by a version bump in one of the first two numbers. That syntax didn't work under testing, but HaXml = 1.13.2, HaXml 1.19 did the trick. Really? That's certainly supposed to work. Can you give more details we can use to reproduce the problem. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Control.Parallel.Strategies
Hi, I was toying with the Control.Parallel.Strategies library, but can't seem to get it to actually do anything in parallel! Here's the code: import System.Random import Control.Parallel.Strategies fib :: Int - Int fib 0 = 1 fib 1 = 1 fib n = fib (n-1) + fib (n-2) main = print $ parMap rnf fib $ take 80 $ randomRs (30,35) (mkStdGen 123) I compile with -threaded, and run with +RTS -N2 -RTS, but yet it stays at 50% on my dual core machine! I should point out that any manual threading with forkIO does indeed use 100% of the CPU, and this problem happens on my work computer too (Vista on my home computer, XP on the work one). Anything I'm missing here? Thanks, -- Sebastian Sylvan +44(0)7857-300802 UIN: 44640862 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Control.Parallel.Strategies
2008/4/9 Sebastian Sylvan [EMAIL PROTECTED]: main = print $ parMap rnf fib $ take 80 $ randomRs (30,35) (mkStdGen 123) Does the strategy rwhnf do it for you? Justin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Control.Parallel.Strategies
On Wed, Apr 9, 2008 at 10:22 PM, Justin Bailey [EMAIL PROTECTED] wrote: 2008/4/9 Sebastian Sylvan [EMAIL PROTECTED]: main = print $ parMap rnf fib $ take 80 $ randomRs (30,35) (mkStdGen 123) Does the strategy rwhnf do it for you? Justin Nope! This is GHC 6.8.2 btw, downloaded the binary from the web site, so it's nothing strange. -- Sebastian Sylvan +44(0)7857-300802 UIN: 44640862 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Control.Parallel.Strategies
On Wed, Apr 9, 2008 at 2:25 PM, Sebastian Sylvan [EMAIL PROTECTED] wrote: Nope! This is GHC 6.8.2 btw, downloaded the binary from the web site, so it's nothing strange. On my hyper-threaded CPU, your original code works fine. With -N2, I see 100% CPU. With N1, only 50%. I am also using GHC 6.8.2. Justin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Control.Parallel.Strategies
On Wed, Apr 9, 2008 at 10:58 PM, Justin Bailey [EMAIL PROTECTED] wrote: On Wed, Apr 9, 2008 at 2:25 PM, Sebastian Sylvan [EMAIL PROTECTED] wrote: Nope! This is GHC 6.8.2 btw, downloaded the binary from the web site, so it's nothing strange. On my hyper-threaded CPU, your original code works fine. With -N2, I see 100% CPU. With N1, only 50%. I am also using GHC 6.8.2. Justin Hmm, that's curious. I compile with ghc --make -threaded partest.hs -o par.exe, and then run it with par.exe +RTS -N2 -RTS. Am I making some silly configuration error? Are you running this on windows? -- Sebastian Sylvan +44(0)7857-300802 UIN: 44640862 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Control.Parallel.Strategies
On Wed, Apr 9, 2008 at 3:03 PM, Sebastian Sylvan [EMAIL PROTECTED] wrote: Hmm, that's curious. I compile with ghc --make -threaded partest.hs -o par.exe, and then run it with par.exe +RTS -N2 -RTS. Am I making some silly configuration error? Are you running this on windows? Yep, that's the command line I used and I am running XP. Justin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Lock-Free Data Structures using STMs in Haskell
Bryan O'Sullivan [EMAIL PROTECTED] writes:
Pete Kazmier wrote:
data ArrayBlockingQueueSTM e = ArrayBlockingQueueSTM {
[...]
sa :: Array Int (TVar e)
}
It's unclear to me why the Array's elements must be wrapped in TVars.
To allow them to be modified. You can't otherwise modify the elements
of an array without going into the ST monad.
Thanks! I forgot about the whole immutable thing :-) Haven't used
arrays yet while learning Haskell!
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Pattern match failure
I'm trying to write a function to recognize a context free grammar, but I keep getting pattern match failure errors. This is what I have: data Grammar c = Brule c c c | Rule c c gez = [(Brule 'S' 'p' 'D'),(Brule 'D' 't' 'E'),(Rule 'E' 'j')] recog :: String - String - [Grammar Char] - Bool recog a b list = case list of [Brule x y z] - if a == [x] then recog [z] b list else recog a b list [Rule x y] - True how can I solve this pattern matching error? -- View this message in context: http://www.nabble.com/Pattern-match-failure-tp16600643p16600643.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Pattern match failure
On Thu, Apr 10, 2008 at 2:05 AM, Jackm139 [EMAIL PROTECTED] wrote: I'm trying to write a function to recognize a context free grammar, but I keep getting pattern match failure errors. This is what I have: data Grammar c = Brule c c c | Rule c c gez = [(Brule 'S' 'p' 'D'),(Brule 'D' 't' 'E'),(Rule 'E' 'j')] recog :: String - String - [Grammar Char] - Bool recog a b list = case list of [Brule x y z] - if a == [x] then recog [z] b list else recog a b list [Rule x y] - True I am stumped as to what this function is trying to do. But your pattern matches are not total; in particular you only handle lists of a single element. I suggest either: recog a b list = case list of (Brule x y z : rules) - ... (involving 'rules') (Rule x y : rules) - ...(involving 'rules') [] - ... (case for the empty list) Or: recog a b (rule:rules) = case rule of Brule x y z - ... Rule x y - ... recog a b [] = ... But the point is that you have to say how to handle lists of more thn one element. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Claus Reinke: type family Id a type instance Id Int = Int foo :: Id a - Id a foo = id n foo' :: Id a - Id a foo' = foo type function notation is slightly misleading, as it presents qualified polymorphic types in a form usually reserved for unqualified polymorphic types. rewriting foo's type helped me to see the ambiguity that others have pointed out: foo :: r ~ Id a = r - r there's nowhere to get the 'a' from. so unless 'Id' itself is fully polymorphic in 'a' (Id a = a, Id a = Int, ..), 'foo' can't really be used. for each type variable, there needs to be at least one position where it is not used as a type family parameter. Yes. It is generally so that the introduction of indexed types (ie, all of GADTs, data type families, or synonym families) means that a type with a parameter is not necessarily parametric. it might be useful to issue an ambiguity warning for such types? The problem is that testing for ambiguity is, in general, difficult. Whether a context is ambiguous depends for example on the currently visible class instances. As a result, a signature that is ambiguous in a module M, may be fine in a module N that imports M. However, I think what should be easier is to improve the error messages given when a function with an ambiguous signature is used. For example, if the error message in the definition of foo' would have included a hint saying that the definition is illegal because its right hand side contains the use of a function with an ambiguous signature, then Ganesh may have had an easier time seeing what's happening. ps. i find these examples and discussions helpful, if often initially puzzling - they help to clear up weak spots in the practice of type family use, understanding, and implementation, thereby improving all while making families more familiar!-) Absolutely! Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Lennart Augustsson: On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann [EMAIL PROTECTED] wrote: 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 I'm referring to the situation where the type inferred by the type checker is illegal for me to put into the program. In our example we can fix this in two ways, by making foo' illegal even when it has no signature, or making foo' legal even when it has a signature. To make it illegal: If foo' has no type signature, infer a type for foo', insert this type as a signature and type check again. If this fails, foo' is illegal. That would be possible, but it means we have to do this for all bindings in a program (also all lets bindings etc). To make it legal: If foo' with a type signature doesn't type check, try to infer a type without a signature. If this succeeds then check that the type that was inferred is alpha-convertible to the original signature. If it is, accept foo'; the signature doesn't add any information. This harder, if not impossible. What does it mean for two signatures to be alpha-convertible? I assume, you intend that given type S a = Int the five signatures forall a. S a forall b. S b forall a b. S (a, b) Int S Int are all the alpha-convertible. Now, given type family F a b type instance F Int c = Int what about forall a. F a Int forall a. F Int Int forall a. F Int a forall a b. (a ~ Int) = F a b and so on So, I guess, you don't really mean alpha-convertible in its original syntactic sense. We should accept the definition if the inferred and the given signature are in some sense equivalent. For this equivalence to be robust, I am sure we need to define it as follows, where = is standard type subsumption: t1 equivalent t2 iff t1 = t2 and t2 = t1 However, the fact that we cannot decide type subsumption for ambiguous types is exactly what led us to the original problem. So, nothing has been won. Summary ~~~ Trying to make those definitions that are currently only legal *without* a signature also legal when the inferred signature is added (foo' in Ganesh's example) doesn't seem workable. However, to generally reject the same definitions, even if they are presented without a signature, seems workable. It does require the compiler to compute type annotations, and then, check that it can still accept the annotated program. This makes the process of type checking together with annotating the checked program idempotent, which is nice. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: type families and type signatures
apfelmus: Manuel M T Chakravarty wrote: apfelmus: Manuel M T Chakravarty wrote: Let's alpha-rename the signatures and use explicit foralls for clarity: foo :: forall a. Id a - Id a foo' :: forall b. Id b - Id b GHC will try to match (Id a) against (Id b). As Id is a type synonym family, it would *not* be valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.) While in general (Id a ~ Id b) -/- (a ~ b) , parametricity makes it true in the case of foo . For instance, let Id a ~ Int . Then, the signature specializes to foo :: Int - Int . But due to parametricity, foo does not care at all what a is and will be the very same function for every a with Id a ~ Int . In other words, it's as if the type variable a is not in scope in the definition of foo . Be careful, Id is a type-indexed type family and *not* a parametric type. Parametricity does not apply. For more details about the situation with GADTs alone, see Foundations for Structured Programming with GADTs. Patricia Johann and Neil Ghani. Proceedings, Principles of Programming Languages 2008 (POPL'08). Yes and no. In the GADT case, a function like bar :: forall a . GADT a - String is clearly not parametric in a, in the sense that pattern matching on the GADT can specialize a which means that we have some form of pattern matching on the type a . The resulting String may depend on the type a . So, by parametricity, I mean type arguments may not be inspected. [..] However, I have this feeling that bar :: forall a . Id a - String with a type family Id *is* parametric in the sense that no matter what a is, the result always has to be the same. Intuitively, that's because we may not pattern match on the branch of a definition like type instance Id String = .. type instance Id Int= .. .. So, in the special case of foo and foo' , solving Id b ~ Id a by guessing a ~ b is safe since foo is parametric in a . We don't know that. We could have type instance Id [a] = GADT a Just looking at the signature, we don't know. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Lennart Augustsson:
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.
The problem of ambiguity is not at all restricted to TFs. In fact,
you need neither TFs nor FDs to get the exact same behaviour. You
don't even need MPTCs:
{-# LANGUAGE FlexibleContexts #-}
module Ambiguity where
class C a
bar :: C (a, b) = b - b
bar = id
bar' :: C (a, b) = b - b
bar' = bar
This gives us
/Users/chak/Code/haskell/Ambiguity.hs:10:7:
Could not deduce (C (a, b)) from the context (C (a1, b))
arising from a use of `bar'
at /Users/chak/Code/haskell/Ambiguity.hs:10:7-9
Possible fix:
add (C (a, b)) to the context of the type signature for `bar''
or add an instance declaration for (C (a, b))
In the expression: bar
In the definition of `bar'': bar' = bar
So, we have this problem as soon as we have flexible contexts and/or
MPTCs, independent of TFs and FDs.
Manuel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance Monad m = Functor m
G'day all. Quoting Jules Bean [EMAIL PROTECTED]: Other solutions, such as class Functor m = Monad m are frequently discussed. I see no H' ticket for it, though. Then add it. :-) You'll probably want to make it depend on Ticket #101, because making class hierarchies more granular generally depends on flexible instances. Cheers, Andrew Bromage ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
