Hi all,
I have encoded a type family such that: type family F a :: * -> * and a function (I know it is complicated, but I think the problem is self explanatory): hyloPara :: (Functor (F a), Functor (F d), F d a ~ F a (a,a), F d c ~ F a (c,a)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c
hyloPara d g h = g . fmap (hyloPara d g h) . h it all works fine. However, if I change the declaration to (changed F d c for the "supposedly equivalent" F a (c,a)):
hyloPara :: (Functor (F a), Functor (F d), F d a ~ F a (a,a), F d c ~ F a (c,a)) => d -> (F a (c,a) -> c) -> (a -> F d a) -> a -> c and I get Occurs check: cannot construct the infinite type: c = (c, a)
When generalising the type(s) for `hyloPara' This really messes up my notions on equality constraints, is it the expected behavior? It would be essential for me to provide this definition. Thanks,
hugo _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Hi Hugo, > I have encoded a type family such that: > > type family F a :: * -> * > > and a function (I know it is complicated, but I think the problem is self > explanatory): > > hyloPara :: (Functor (F a), Functor (F d), F d a ~ F a (a,a), F d c ~ F a > (c,a)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c > hyloPara d g h = g . fmap (hyloPara d g h) . h > > it all works fine. > > However, if I change the declaration to (changed F d c for the > "supposedly equivalent" F a (c,a)): > > hyloPara :: (Functor (F a), Functor (F d), F d a ~ F a (a,a), F d c ~ F a > (c,a)) => d -> (F a (c,a) -> c) -> (a -> F d a) -> a -> c > > and I get > > Occurs check: cannot construct the infinite type: c = (c, a) > When generalising the type(s) for `hyloPara' > > This really messes up my notions on equality constraints, is it the expected > behavior? It would be essential for me to provide this definition. I think you've uncovered a bug in the type checker. We made the design choice that type functions with a higher-kinded result type must be injective with respect to the additional paramters. I.e. in your case: F x y ~ F u v <=> F x ~ F u /\ y ~ v So if we apply that to F d c ~ F a (c,a) we get: F d ~ F a /\ c ~ (c,a) where the latter clearly is an occurs-check error, i.e. there's no finite type c such that c = (c,a). So the error in the second version is justified. There should have been one in the latter, but the type checker failed to do the decomposition: a bug. What instances do you have for F? Are they such that F d c ~ F a (c,a) can hold? By the way, for your function, you don't need equations in your type signature. This will do: hyloPara :: Functor (F d) => d -> (F d c -> c) -> (a -> F d a) -> a -> c Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: [hidden email] url: http://www.cs.kuleuven.be/~toms/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
I know I do not need these constraints, it was just the simplest way I found to explain the problem.
I have fought about that: I was not expecting F d c ~ F a (c,a) not mean that F d ~F a /\ c ~(c,a), I thought the whole family was "parameterized". If I encoded the family type family F a x :: * F d c ~ F a (c,a) would be semantically different, meaning that this "decomposition rule" does not apply? Thanks, hugo _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Tue, 11 Mar 2008, Hugo Pacheco wrote:
> I know I do not need these constraints, it was just the simplest way I found > to explain the problem. > > I have fought about that: I was not expecting F d c ~ F a (c,a) not mean > that F d ~F a /\ c ~(c,a), I thought the whole family was "parameterized". > If I encoded the family > > type family F a x :: * > > F d c ~ F a (c,a) would be semantically different, meaning that this > "decomposition rule" does not apply? Correct. However, then you cannot write "Functor (F a)" because type functions must be fully applied. So either way you have a problem. Could you show the type instances for F you have (in mind)? This way we can maybe see whether what you want to is valid and the type checker could be adjusted to cope with it, or whether what you're trying to do would not be valid (in general). I have my suspicions about your mentioning of both Functor (F d) and Functor (F a) in the signature. Which implementation of fmap do you want? Or should they be both the same (i.e. F d ~ F a)? Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: [hidden email] url: http://www.cs.kuleuven.be/~toms/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Yes, I have tried both implementations at the start and solved it by choosing for the following:
type family F a :: * -> * type FList a x = Either () (a,x)
type instance F [a] = FList a instance (Functor (F [a])) where fmap _ (Left _) = Left ()
fmap f (Right (a,x)) = Right (a,f x) The option was: type family F a x :: * type instance F [a] x = Either() (a,x) instance (Functor (F [a])) where -- error, not enough parameters passed to F
fmap _ (Left _) = Left () fmap f (Right (a,x)) = Right (a,f x) So, indeed, with either implementation I have a problem. >I have my suspicions about your mentioning of both Functor (F d) and >Functor (F a) in the signature. Which implementation of fmap do you want? >Or should they be both the same (i.e. F d ~ F a)? This is an hard question to which the answer is both. In the definition of an hylomorphism I want the fmap from (F d): hylo :: (Functor (F d)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c hylo d g h = g . fmap (hylo d g h) . h
However, those constraints I have asked about would allow me to encode a paramorphism as an hylomorphism:
class Mu a where inn :: F a a -> a out :: a -> F a a para :: (Mu a, Functor (F a),Mu d, Functor (F d),F d a ~ F a (a,a), F d c ~ F a (c,a)) => d -> (F a (c,a) -> c) -> a -> c
para d f = hylo d f (fmap (id /\ id) . out) In para, I would want the fmap from (F a) but that would be implicitly forced by the usage of out :: a -> F a a
Sorry for all the details, ignore them if they are too confusing. Do you think there might be a definition that would satisfy me both Functor instances and equality?
Thanks for your pacience, hugo _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Tue, 11 Mar 2008, Hugo Pacheco wrote:
> Yes, I have tried both implementations at the start and solved it by > choosing for the following: > type family F a :: * -> * > type FList a x = Either () (a,x) > type instance F [a] = FList a > > instance (Functor (F [a])) where > fmap _ (Left _) = Left () > fmap f (Right (a,x)) = Right (a,f x) For this implementation we do have that F [a] b ~ F [c] d <=> F [a] ~ F [c] /\ b ~ d Right? So for this instance, your para via hylo wouldn't work anyway. I'd like to see some type instances and types such that the equation F d a ~ F a (a,a) holds. With your example above, it's not possible to make the equation hold, .e.g. F [t] [s] ~ F [s] ([s],[s]) <=> Either () (t,[s]) ~ Either ()(s,([s],[s])) is not true for any (finite) types t and s. Do you have such an example? You should have one, if you want to be able to call para. Tom >> I have my suspicions about your mentioning of both Functor (F d) and >> Functor (F a) in the signature. Which implementation of fmap do you want? >> Or should they be both the same (i.e. F d ~ F a)? > > This is an hard question to which the answer is both. > > In the definition of an hylomorphism I want the fmap from (F d): > > hylo :: (Functor (F d)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c > hylo d g h = g . fmap (hylo d g h) . h > > However, those constraints I have asked about would allow me to encode a > paramorphism as an hylomorphism: > > class Mu a where > inn :: F a a -> a > out :: a -> F a a > > para :: (Mu a, Functor (F a),Mu d, Functor (F d),F d a ~ F a (a,a), F d c ~ > F a (c,a)) => d -> (F a (c,a) -> c) -> a -> c > para d f = hylo d f (fmap (id /\ id) . out) > > In para, I would want the fmap from (F a) but that would be implicitly > forced by the usage of out :: a -> F a a > > Sorry for all the details, ignore them if they are too confusing. > Do you think there might be a definition that would satisfy me both Functor > instances and equality? > > Thanks for your pacience, > hugo > -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: [hidden email] url: http://www.cs.kuleuven.be/~toms/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
That's simple Tom.
Imagine the factorial function for Int written as a paramorphism: type instance F Int = Either One instance (Mu Int) where inn (Left _) = 0 inn (Right n) = succ n out 0 = Left () out n = Right (pred n) instance Functor (F Int) where fmap _ (Left ()) = Left () fmap f (Right n) = Right (f n) fact :: Int -> Int fact = para (const 1 \/ (uncurry (*)) . (id >< succ)) If we consider that the paramorphism is implemented as an hylomorphism, then an intermediate virtual type (d in the hylo definition) [Int] If you test the constraints for d = [Int], a = Int and c = Int F d c ~ F a (c,a) F d a = F [Int] Int = Either One (Int,Int) F a (c,a) = F Int (Int,Int) = Either One (Int,Int) F d a ~ F a (a,a) F d a = F a (a,a) -- pure substitution of the above case Hope this helps. Thanks again for you patience, hugo _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Tom Schrijvers-2
>> type family F a :: * -> *
.. > We made the design > choice that type functions with a higher-kinded result type must be > injective with respect to the additional paramters. I.e. in your case: > > F x y ~ F u v <=> F x ~ F u /\ y ~ v i'm still trying to understand this remark: - if we are talking about "type functions", i should be allowed to replace a function application with its result, and if that result doesn't mention some parameters, they shouldn't play a role at any stage, right? - if anything other than the function result matters, isn't it somewhat misleading to speak of "type functions"? - if the parameters have to match irrespective of whether they appear in the result, that sounds like phantom types. ok, but we're talking about a system that mixes unification with rewriting, so shouldn't the phantom parameters be represented in all rewrite results, just to make sure they cannot be ignored in any contexts? ie, with type instance F a = <rhs> F a x should rewrite not to <rhs>, but to <rhs>_x, which would take care of the injectivity you want in the ~-case, but would also preserve the distinction if rewriting should come before ~, even if <rhs> managed to consume x, by being a constant function on types. - things seem to be going wrong in the current implementation. consider this code, accepted by GHCi, version 6.9.20080317: ------------------------------------------ {-# LANGUAGE TypeFamilies #-} type family Const a :: * -> * type instance Const a = C a type C a t = a f :: Const Bool Int -> Const Bool Char -> Const Bool Bool f i c = False -- f i c = i f i c = i && True f i c = (i || c) ------------------------------------------ (note the partially applied type synonym in the type instance, which is a constant function on types). it looks as if: - False::Bool is accepted as Const Bool Bool - i::Const Bool Int is accepted as Bool - c::Const Bool Char is accepted as Bool - both i and c are accepted as Bool, so seem to be of an equivalent type, but aren't really.. - i::Const Bool Int is not accepted as Const Bool Char directly, but is accepted via one of the "eta expansions" for Bool, namely (&&True) my current guess is that the implementation is incomplete, but that the idea of "type functions" also needs to be adjusted to take your design decision into account, with "phantom types" and type parameter annotations for type function results suggesting themselves as potentially helpful concepts? or, perhaps, the implication isn't quite correct, and type parameters shouldn't be unified unless they appear in the result of applying the type function? the implementation would still be incomplete, but instead of rejecting more of the code, it should allow the commented-out case as well? could you please help me to clear up this confusion?-) thanks, claus _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
> could you please help me to clear up this confusion?-)
Let me summarize :-) The current design for type functions with result kinds other than * (e.g. * -> *) has not gotten very far yet. We are currently stabilizing the ordinary * type functions, and writing the story up. When that's done we can properly focus on this issue and consider different design choices. Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: [hidden email] url: http://www.cs.kuleuven.be/~toms/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Claus Reinke
>>> type family F a :: * -> *
> .. >> We made the design >> choice that type functions with a higher-kinded result type must be >> injective with respect to the additional paramters. I.e. in your case: >> >> F x y ~ F u v <=> F x ~ F u /\ y ~ v actually, i don't even understand the first part of that:-( why would F x and F u have to be the same functions? shouldn't it be sufficient for them to have the same result, when applied to y and v, respectively? consider: -------------------------------------- type family G1 a :: * -> * type instance G1 a = G3 type family G2 a :: * -> * type instance G2 a = G4 type family G3 a :: * type instance G3 Bool = Bool type instance G3 Char = Bool type family G4 a :: * type instance G4 Bool = Char type instance G4 Char = Bool h :: G1 a Bool ~ G2 a Char => G1 a Bool h = True -------------------------------------- for which GHCi, version 6.9.20080317 happily infers *Main> :t h h :: G1 a Bool *Main> h True even though G1 a ~ G3 ~/~ G4 ~ G2 a ? claus > i'm still trying to understand this remark: > > - if we are talking about "type functions", i should be allowed > to replace a function application with its result, and if that > result doesn't mention some parameters, they shouldn't > play a role at any stage, right? > > - if anything other than the function result matters, isn't it > somewhat misleading to speak of "type functions"? > > - if the parameters have to match irrespective of whether > they appear in the result, that sounds like phantom types. > > ok, but we're talking about a system that mixes unification > with rewriting, so shouldn't the phantom parameters be > represented in all rewrite results, just to make sure they > cannot be ignored in any contexts? > > ie, with > > type instance F a = <rhs> > > F a x should rewrite not to <rhs>, but to <rhs>_x, > which would take care of the injectivity you want in the > ~-case, but would also preserve the distinction if > rewriting should come before ~, even if <rhs> managed > to consume x, by being a constant function on types. > > - things seem to be going wrong in the current implementation. > consider this code, accepted by GHCi, version 6.9.20080317: > ------------------------------------------ > {-# LANGUAGE TypeFamilies #-} > > type family Const a :: * -> * > type instance Const a = C a > type C a t = a > > f :: Const Bool Int -> Const Bool Char -> Const Bool Bool > f i c = False > -- f i c = i > f i c = i && True > f i c = (i || c) > ------------------------------------------ > > (note the partially applied type synonym in the type instance, > which is a constant function on types). it looks as if: > > - False::Bool is accepted as Const Bool Bool > - i::Const Bool Int is accepted as Bool > - c::Const Bool Char is accepted as Bool > - both i and c are accepted as Bool, so seem to be of > an equivalent type, but aren't really.. > - i::Const Bool Int is not accepted as Const Bool Char > directly, but is accepted via one of the "eta expansions" > for Bool, namely (&&True) > > my current guess is that the implementation is incomplete, > but that the idea of "type functions" also needs to be adjusted > to take your design decision into account, with "phantom types" > and type parameter annotations for type function results > suggesting themselves as potentially helpful concepts? > > or, perhaps, the implication isn't quite correct, and > type parameters shouldn't be unified unless they appear > in the result of applying the type function? the implementation > would still be incomplete, but instead of rejecting more of the > code, it should allow the commented-out case as well? > > could you please help me to clear up this confusion?-) > > thanks, > claus > > > > _______________________________________________ > Haskell-Cafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Tom Schrijvers-2
> Let me summarize :-)
> > The current design for type functions with result kinds other than * > (e.g. * -> *) has not gotten very far yet. We are currently stabilizing > the ordinary * type functions, and writing the story up. When that's done > we can properly focus on this issue and consider different design choices. thanks, seems i was too optimistic, then!-) btw, i noticed that the user guide points to the haskell wiki only, while the latest info seems to be on the ghc wiki. given the number of variations and the scope of development, it would also be helpful if the user guide had at least a one-paragraph executive summary of the state of play, dated to clarify how up-to-date that summary is. that would avoid discussions of not yet stabilized features (should ghc issue a warning when such are used?). claus _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Claus Reinke
Claus Reinke:
>>> type family F a :: * -> * > .. >> We made the design choice that type functions with a higher-kinded >> result type must be injective with respect to the additional >> paramters. I.e. in your case: >> F x y ~ F u v <=> F x ~ F u /\ y ~ v > > i'm still trying to understand this remark: > > - if we are talking about "type functions", i should be allowed > to replace a function application with its result, and if that > result doesn't mention some parameters, they shouldn't > play a role at any stage, right? > > - if anything other than the function result matters, isn't it > somewhat misleading to speak of "type functions"? You will notice that I avoid calling them "type functions". In fact, the official term is "type families". That is what they are called in the spec <http://haskell.org/haskellwiki/GHC/Type_families> and GHC's option is -XTypeFamilies, too. More precisely, they are "type-indexed type families". One difference between type families and (value-level) functions is that not all parameters of a type family are treated the same. A type family has a fixed number of type indicies. We call the number of type indicies the type family's arity and by convention, the type indicies come always before other type parameters. In the example type family F a :: * -> * F has arity 1, whereas type family G a b :: * has arity 2. So, the number of named parameters given is the arity. (The overall kind is still F :: * -> * -> *; ie, the arity is not obvious from the kind, which I am somewhat unhappy about.) In other words, in a type term like (F Int Bool), the two parameters Int and Bool are treated differently. Int is treated like a parameter to a function (which is what you where expecting), whereas Bool is treated like a parameter to a vanilla data constructor (the part you did not expect). To highlight this distinction, we call only Int a type index. Generally, if a type family F has arity n, it's first n parameters are type indicies, the rest are treated like the parameters of any other type constructor. Moreover, a type family of arity n, must always be applied to at least n parameters - ie, applications to type indicies cannot be partial. This is not just an arbitrary design decision, it is necessary to stay compatible with Haskell's existing notion of higher-kinded unification (see, Mark Jones' paper about constructor classes), while keeping the type system sound. To see why, consider that Haskell's higher-kinded type system, allows type terms, such as (c a), here c may be instantiated to be (F Int) or Maybe. This is only sound if F treats parameters beyond its arity like any other type constructor. A more formal discussion is in our TLDI paper about System F_C(X). Manuel _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Tom Schrijvers-2
Tom Schrijvers:
>> could you please help me to clear up this confusion?-) > > Let me summarize :-) > > The current design for type functions with result kinds other than * > (e.g. * -> *) has not gotten very far yet. We are currently > stabilizing the ordinary * type functions, and writing the story up. > When that's done we can properly focus on this issue and consider > different design choices. I don't quite agree. The current story was pretty much settled in the paper on associated type synonyms already and further clarified in the FC paper. Manuel _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Claus Reinke
Claus Reinke:
>>>> type family F a :: * -> * >> .. >>> We made the design choice that type functions with a higher-kinded >>> result type must be injective with respect to the additional >>> paramters. I.e. in your case: >>> F x y ~ F u v <=> F x ~ F u /\ y ~ v > > actually, i don't even understand the first part of that:-( > > why would F x and F u have to be the same functions? > shouldn't it be sufficient for them to have the same result, > when applied to y and v, respectively? Oh, yes, that is sufficient and exactly what is meant by F x ~ F u. It means, the two can be unified modulo any type instances and local given equalities. Manuel _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Manuel M T Chakravarty
>>>> type family F a :: * -> *
>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v >> > words, in a type term like (F Int Bool), the two parameters Int and > Bool are treated differently. Int is treated like a parameter to a > function (which is what you where expecting), whereas Bool is treated > like a parameter to a vanilla data constructor (the part you did not > expect). To highlight this distinction, we call only Int a type > index. Generally, if a type family F has arity n, it's first n > parameters are type indicies, the rest are treated like the parameters > of any other type constructor. i'm not sure haskell offers the kind of distinction that we need to talk about this: 'data constructor' is value-level, 'type constructor' doesn't distinguish between type- vs data-defined type constructors. i think i know what you mean, but it confuses me that you use 'data constructor' (should be data/newtype-defined type constructor?) and 'type constructor' (don't you want to exclude type-defined type constructors here). data ConstD x y = ConstD x type ConstT x y = x 'ConstD x' and 'ConstT x' have the same kind, that of type constructors: * -> *. but: ConstD x y1 ~ ConstD x y2 => y1 ~ y2 whereas forall y1, y2: ConstT x y1 ~ ConstT x y2 and i thought 'type family' was meant to suggest type synonym families, in contrast to 'data family'? you did notice that i gave an example of how ghc does not seem to follow that decomposition rule, didn't you? ghc seems to behave almost as i would expect, not as the decomposition rule seems to suggest. still confused, claus _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Manuel M T Chakravarty
>>>>> type family F a :: * -> *
>>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v >> >> why would F x and F u have to be the same functions? >> shouldn't it be sufficient for them to have the same result, >> when applied to y and v, respectively? > > Oh, yes, that is sufficient and exactly what is meant by F x ~ F u. > It means, the two can be unified modulo any type instances and local > given equalities. sorry, i don't understand how that could be meant by 'F x ~ F u'; that equality doesn't even refer to any specific point on which these two need to be equal, so it can only be a point-free higher-order equality, can't it? the right-to-left implication is obvious, but the left-to-right implication seems to say that, for 'F x' and 'F u' to be equal on any concrete pair of types 'y' and 'u', they have to be equal on all possible types and 'y' and 'u' themselves have to be equal. again, i gave a concrete example of how ghc behaves as i would expect, not as that decomposition rule would suggest. i'll try to re-read the other paper you suggested, but it would help me if you could discuss the two concrete examples i gave in this thread. thanks, claus _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Claus Reinke
Claus Reinke:
>>>>> type family F a :: * -> * >>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v >>> >> words, in a type term like (F Int Bool), the two parameters Int >> and Bool are treated differently. Int is treated like a parameter >> to a function (which is what you where expecting), whereas Bool is >> treated like a parameter to a vanilla data constructor (the part >> you did not expect). To highlight this distinction, we call only >> Int a type index. Generally, if a type family F has arity n, it's >> first n parameters are type indicies, the rest are treated like >> the parameters of any other type constructor. > > i'm not sure haskell offers the kind of distinction that we > need to talk about this: 'data constructor' is value-level, > 'type constructor' doesn't distinguish between type- vs > data-defined type constructors. i think i know what you > mean, but it confuses me that you use 'data constructor' > (should be data/newtype-defined type constructor?) Yes, I meant to write "data type constructor". > and 'type constructor' (don't you want to exclude > type-defined type constructors here). It may have been clearer if I had written data type constructor, but then the Haskell 98 report doesn't bother with that either (so I tend to be slack about it, too). > data ConstD x y = ConstD x > type ConstT x y = x > > 'ConstD x' and 'ConstT x' have the same kind, that > of type constructors: * -> *. but: > > ConstD x y1 ~ ConstD x y2 => y1 ~ y2 > > whereas > > forall y1, y2: ConstT x y1 ~ ConstT x y2 But note that ConstT x ~ ConstT x is malformed. > and i thought 'type family' was meant to suggest type > synonym families, in contrast to 'data family'? My nomenclature is as follows. The keywords 'type family' introduces a "type synonym family" and 'data family' introduces a "data type family" (or just "data family"). The term "type family" includes both. This follows Haskell's common use of "type constructor", "type synonym constructor", and "data type constructor". > you did notice that i gave an example of how ghc does > not seem to follow that decomposition rule, didn't you? Yes, but I didn't see why you think GHC does the wrong thing. Manuel _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Claus Reinke
Claus Reinke:
>>>>>> type family F a :: * -> * >>>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v >>> >>> why would F x and F u have to be the same functions? >>> shouldn't it be sufficient for them to have the same result, >>> when applied to y and v, respectively? >> Oh, yes, that is sufficient and exactly what is meant by F x ~ F >> u. It means, the two can be unified modulo any type instances and >> local given equalities. > > sorry, i don't understand how that could be meant by 'F x ~ F u'; > that equality doesn't even refer to any specific point on which these > two need to be equal, so it can only be a point-free higher-order > equality, can't it? > > the right-to-left implication is obvious, but the left-to-right > implication seems to say that, for 'F x' and 'F u' to be equal on > any concrete pair of types 'y' and 'u', they have to be equal on all > possible types and 'y' and 'u' themselves have to be equal. You write 'y' and 'u'. Do you mean 'x' and 'u'? If so, why do you think the implication indicates that x and u need to be the same? > again, i gave a concrete example of how ghc behaves as i would > expect, not as that decomposition rule would suggest. Maybe you can explain why you think so. I didn't understand why you think the example is not following the decomposition rule. Manuel _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Manuel M T Chakravarty:
>> again, i gave a concrete example of how ghc behaves as i would >> expect, not as that decomposition rule would suggest. > > Maybe you can explain why you think so. I didn't understand why you > think the example is not following the decomposition rule. Actually, see http://hackage.haskell.org/trac/ghc/ticket/2157#comment:10 Manuel _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
>>> again, i gave a concrete example of how ghc behaves as i would
>>> expect, not as that decomposition rule would suggest. >> >> Maybe you can explain why you think so. I didn't understand why you >> think the example is not following the decomposition rule. > > Actually, see > > http://hackage.haskell.org/trac/ghc/ticket/2157#comment:10 > > Manuel for those following along here: | However, I think I now understand what you are worried about. It is the | interaction of type families and GHC's generalised type synonyms (i.e., | type synonyms that may be partially applied). I agree that it does lead | to an odd interaction, because the outcome may depend on the order in | which the type checker performs various operations. In particular, | whether it first applies a type instance declaration to reduce a type | family application or whether it first performs decomposition. yes, indeed, thanks! that was the central point of example one. one might say that the central point of example two were two partially applied type synonym families in the same position (rhs of a type synonym family instance definition). usually, when reduction meets typing, there is a subject reduction theorem, stating that types do not change during reduction. since, in this case, reduction and constraint generation happen at the same (type) level, the equivalent would be a proof of confluence, so that it doesn't matter which type rules are applied in which order (in this case, decomposition and reduction). as far as i could determine, the TLDI paper does not deal with the full generality of ghc's type extensions, so it doesn't stumble over this issue, and might need elaboration. my suggestion was to annotate the results of type family application reductions with the type parameters. in essence, that would carry the phantom types along for type checking, and the decomposition rule could be taken care of even after reduction, by comparing these annotations. alternatively, use the decomposition rule as the reduction rule. both would make clear that one is *not* dealing with simple type-level function applications. | The most clean solution may indeed be to outlaw partial applications of | vanilla type synonyms in the rhes of type instances. (Which is what I | will implement unless anybody has a better idea.) i always dislike losing expressiveness, and ghc does almost seem to behave as i would expect in those examples, so perhaps there is a way to fit the partial applications into the theory of your TLDI paper. and i still don't like the decomposition rule, and i still don't even understand that first part about comparing partially applied type constructors!-) but in terms of actually implementing your design, and matching your theory and proofs, it might be best to treat the rhs of a type family instance like a type class instance parameter (where partial applications of synonyms and families are ruled out), not like the rhs of a type synonym definition (where everything is allowed). then users can try out an implementation that does what you say it would, including constraints needed for your proofs, which might lead to extension requests later - as Tom said, there may still be some open ends. perhaps you could keep those two examples around in a separate ticket, collecting experiences with and limitations of type families? thanks, claus _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |