Re: [Haskell-cafe] Issues(Bugs?) with GHC Type Families
Hugo Pacheco: If the equality does not hold, you should get a type error because your program is not type correct. So, what is it that you would like different? I would simply like the compiler not to use that instance if the equality constraint does not hold, like some another instance dependency constraint, but I assume that is not possible. This is independent of type families. The selection of type class instances does *never* dependent on the instance context, only on the instance head. I know that this is sometimes annoying, but type checking would be a a lot more complicated/expensive without that rule. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Issues(Bugs?) with GHC Type Families
On Fri, Mar 7, 2008 at 2:10 AM, Ryan Ingram [EMAIL PROTECTED] wrote: I don't think the cost is that great; the compiler can easily flag polymorphic functions that require type information for some or all arguments and in many cases the type evidence can be passed just-in-time when calling from a non-polymorphic function into a polymorphic function. As I understand it, the cost in performance isn't too bad. For example, JHC uses type-passing to implement type classes. One problem is that a language with pervasive typecase has weaker guarantees. For example, in present-day Haskell we can tell that length :: [a] - Int works the same for every type 'a' just by looking at the type signature. That's not the case if we can call typecase in arbitrary functions. We can avoid that problem by requiring a type representation parameter, or otherwise indicating the use of typecase in the signature. Modern Haskell provides this with the Typeable class. (Which, in JHC, is essentially empty.) Thus, another solution for writing the show instance for lists is: class (Typeable a) = Show [a] where show s = case cast s of Just str - \ ++ str ++\ Nothing - showList s where showList ... To summarize: we can make more claims about a function with type forall a. F a - G a than one with type forall a. (Typeable a) = F a - G a, even though every type can (as far as I know) be made an instance of Typeable. -- Dave Menendez [EMAIL PROTECTED] http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Issues(Bugs?) with GHC Type Families
Hugo Pacheco: Just something I have been wondering. I would like to implement somehting like: type family F a :: * - * ... class C a b where ... instance (F a ~ F b) = C a b where ... But apparently type equality coercions can not be used as a single context. If I enable -fallow-undecidable-instances, whenever the equality does not hold, the instance returns a compile error, what does make sense. Is there any way I could overcome this? I think I don't understand your question fully. This class instance requires both -XFlexibleInstances and -fallow-undecidable-instances to compile. If the equality does not hold, you should get a type error because your program is not type correct. So, what is it that you would like different? Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Issues(Bugs?) with GHC Type Families
If the equality does not hold, you should get a type error because your program is not type correct. So, what is it that you would like different? I would simply like the compiler not to use that instance if the equality constraint does not hold, like some another instance dependency constraint, but I assume that is not possible. hugo ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Issues(Bugs?) with GHC Type Families
What I said is not true since overlapping instances are not that much decidable. Btw, in previous versions of GHC this worked well, but now I suppose order does not suffices to define instances overlapping How could I compile such an example, assuming that I want to use the instance C String for Strings only and the more general instance for the rest? class C a where c :: a instance C Char where c = 'a' instance C a = C [a] where c = [c :: a,c :: a] instance C String where c = a cc = c :: String Sorry for the newbie question. hugo ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Issues(Bugs?) with GHC Type Families
2008/3/6 Hugo Pacheco [EMAIL PROTECTED]: How could I compile such an example, assuming that I want to use the instance C String for Strings only and the more general instance for the rest? class C a where c :: a instance C Char where c = 'a' instance C a = C [a] where c = [c :: a,c :: a] instance C String where c = a cc = c :: String This is actually a general issue with the way typeclasses are defined in Haskell; the accepted solution is what the Show typeclass does: class C a where c :: a cList :: [a] cList = [c,c] instance C Char where c = 'a' cList = a -- replaces instance for String above instance C a = C [a] where c = cList cc = c :: String I don't really like this solution; it feels like a hack and it relies on knowing when you define the typeclass what sort of overlap you expect. I wish there was some form of instance declaration that let you do case analysis; something similar to the following: instances C [a] where instance C String where c = a instance C a = C [a] where c = [c,c] instance Num a = C [a] where c = [0] When trying to find a constraint for C [a] for some type a, the instances would be checked in order: 1) If a was Char, the first instance would be selected. 2) Otherwise, if there was an instance for C a, the second instance would be selected. 3) Otherwise, if there was an instance for Num a, the third instance would be selected. 4) Otherwise a type error would occur. Then overlapping instances wouldn't be required nearly as often; the relevant instances would all have to be defined in one place, but that's often the case anyways. In exchange for giving up some of the openness of typeclasses, you would get the benefit of being able to have better control over instance definitions. You could also use this to create closed typeclasses using instances C a where ...; the compiler would then know that all possible instances were defined at that location; any other definition would clearly overlap and so the compiler could rule out their existence immediately. There might be some benefit in this case in terms of removing ambiguities that currently arise due to open typeclasses. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Issues(Bugs?) with GHC Type Families
On Thu, Mar 6, 2008 at 7:52 PM, Ryan Ingram [EMAIL PROTECTED] wrote: I wish there was some form of instance declaration that let you do case analysis; something similar to the following: instances C [a] where instance C String where c = a instance C a = C [a] where c = [c,c] instance Num a = C [a] where c = [0] When trying to find a constraint for C [a] for some type a, the instances would be checked in order: 1) If a was Char, the first instance would be selected. 2) Otherwise, if there was an instance for C a, the second instance would be selected. 3) Otherwise, if there was an instance for Num a, the third instance would be selected. 4) Otherwise a type error would occur. I agree that this would be nice. But I think that the situation is stickier than it looks on the surface. Consider this: instances GShow [a] where instance [Char] where gShow = id instance [a] where gShow x = list( ++ length x ++ ) gShow' :: [a] - String gShow' = gShow For any implementation which keeps implementations polymorphic (i.e. no required inlining like C++), despite what the program *says*, gShow' would not be equal to gShow. When gShow' calls gShow, it needs a GShow dictionary; so it does constraint solving and finds a dictionary for [a]. a is not Char, so it uses the [a] dictionary, not the [Char] dictionary. Therefore: gShow hello = hello gShow' hello = list(5) That's just the first issue, and that alone is enough to make me not want this. When we get to more complex examples like the one you gave above involving constraints, in order to solve for the constraints needed for an instance of C [a] you need a *disjunction* constraint, which vastly increases the likelihood of an undecidable solution. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Issues(Bugs?) with GHC Type Families
On Thu, Mar 6, 2008 at 9:52 PM, Ryan Ingram [EMAIL PROTECTED] wrote: This is actually a general issue with the way typeclasses are defined in Haskell; the accepted solution is what the Show typeclass does: class C a where c :: a cList :: [a] cList = [c,c] instance C Char where c = 'a' cList = a -- replaces instance for String above instance C a = C [a] where c = cList cc = c :: String I don't really like this solution; it feels like a hack and it relies on knowing when you define the typeclass what sort of overlap you expect. The pattern above can be thought of as a specialized version of this: class C a where c :: a class ListOfC a where listOfC :: [a] instance (ListOfC a) = C [a] where c = listOfC This works for an arbitrary number of type constructors (good!), but requires a ListOfC instance for everything you might want to put into a list (cumbersome!). You can make things slightly less verbose by putting a sensible default in ListOfC, class (C a) = ListOfC a where listOfC :: [a] listOfC = default_c -- Dave Menendez [EMAIL PROTECTED] http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Issues(Bugs?) with GHC Type Families
On Thu, Mar 6, 2008 at 7:16 PM, Luke Palmer [EMAIL PROTECTED] wrote:
I agree that this would be nice. But I think that the situation is
stickier than it looks on the surface. Consider this:
instances GShow [a] where
instance [Char] where gShow = id
instance [a] where gShow x = list( ++ length x ++ )
gShow' :: [a] - String
gShow' = gShow
I'm not so sure. It's not that hard to imagine a compiler where the
core-language expansion of this code looks like this:
data GShowDict a = GShowDict { gShow :: a - String }
id :: (a :: *) - a - a
id A a = a
length :: (a :: *) - [a] - Int
-- definition elided
gShow' :: (a :: *) - [a] - String
gShow' A = gShow (mkDict_GShow_List A)
mkDict_GShow_List :: (a :: *) - GShowDict [a]
mkDict_GShow_List A =
typecase A of
Char - GShowDict (id [A])
_ - GShowDict (\xs - length A xs)
Now, it's true that this means that you can no longer do full type
erasure, but I'm not convinced of the importance of that anyways; if
you look at mainstream languages you generally only get type erasure
for a restricted subset of the types and that's good enough for
performance:
1) In Java, you only get type erasure for primitive types;
everything else needs its type tag so it can be safely downcasted from
Object.
2) In C++ only primitive types and structs/classes with no virtual
functions get type erasure; if a class has virtual functions its
virtual function table is implicitly a type tag.
I don't think the cost is that great; the compiler can easily flag
polymorphic functions that require type information for some or all
arguments and in many cases the type evidence can be passed
just-in-time when calling from a non-polymorphic function into a
polymorphic function.
When we get to more complex examples like the one you gave
above involving constraints, in order to solve for the constraints
needed for an instance of C [a] you need a *disjunction* constraint,
which vastly increases the likelihood of an undecidable solution.
This is definitely an issue. I don't have a full understanding of the
methods used for typechecking/inference of typeclasses; I'm just a
programmer who wants MORE POWER :)
-- ryan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Issues(Bugs?) with GHC Type Families
Just something I have been wondering. I would like to implement somehting like: type family F a :: * - * ... class C a b where ... instance (F a ~ F b) = C a b where ... But apparently type equality coercions can not be used as a single context. If I enable -fallow-undecidable-instances, whenever the equality does not hold, the instance returns a compile error, what does make sense. Is there any way I could overcome this? Thanks, hugo ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Issues(Bugs?) with GHC Type Families
2008/3/3 Hugo Pacheco [EMAIL PROTECTED]: class C a where type S a (k :: * - *) :: * instance C [a] where type S [a] k = (a,k a) does not compile under the claim that the type variable k is not in scope. It's not entirely syntactical sugar; I believe that when a type family is a member of a type-class it makes the assertion that only the class variables are part of the function. In the class declaration: class C a where type S a (k :: * - *) :: * there are two arguments to the type function S, but the class C only provides one. Contrast with the following type Pair a k = (a, k a) class C a where type S a :: (* - *) - * instance C [a] where type S [a] = Pair a datakind Nat = Zero or datakind Nat = Zero | Succ Nat datakinds are listed under future work in the papers I have read; they aren't implemented yet. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Issues(Bugs?) with GHC Type Families
Hugo Pacheco: I have recently tried to replicate some examples from in the articles about type families but found some possible bugs. In [2], the example class C a where type S a (k :: * - *) :: * instance C [a] where type S [a] k = (a,k a) does not compile under the claim that the type variable k is not in scope. However, if we extract the type family from the class type family S a (k :: * - *) :: * type instance S [a] k = (a, k a) class C a it compiles correctly. According to [3], the difference is purely syntactic sugar, does that mean that both examples should compile and behave the same or is there some subtlety that justifies the class example not to compile? I am sorry for the confusion this causes, but we wrote the paper before the implementation in GHC was finalised. Hence, the implementation deviates from the paper in some aspects. Generally, please use http://haskell.org/haskellwiki/GHC/Type_families (which will be integrated into GHC's Users Manual for 6.10) as the definite guide to the implementation. Here a brief rational for this change in design. We originally intended to distinguish between type parameters that do use type indexing (the a in (S a k)) and those that do not (the k in (S a k)).However, we found later that this leads to implementation problems. The new rule is that any explicitly named parmeters, eg, s and k in type family S a (k :: * - *) :: * are indexed. If you don't want to use the second parameter as an index, write type S a :: (* - *) - * This is also simpler to explain, as simply *all* explicitly named parameters in a type family declaration are indicies. Another issue is that data kinds (used in both [2] and [3]) do not seem to be supported at all by the compiler, are they already implemented in GHC? Simple examples such as datakind Nat = Zero or datakind Nat = Zero | Succ Nat fail to compile. No, datakinds aren't supported yet. We still intend to add them, but our first priority is to thoroughly debug the existing functionality and especially to make sure the interaction with GADTs works well. Thanks for the feedback. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
