Re: [Haskell-cafe] Re: Associated Type Synonyms question
Claus Reinke writes: The main argument for ATS is that the extra parameter for the functionally dependend type disappears, but as you say, that should be codeable in FDs. I say should be, because that does not seem to be the case at the moment. My approach for trying the encoding was slightly different from your's, but also ran into trouble with implementations. First, I think you need a per-class association, so your T a b would be specific to C. Second, I'd use a superclass context to model the necessity of providing an associated type, and instance contexts to model the provision of such a type. No big difference, but it seems closer to the intension of ATS: associated types translate into type association constraints. (a lot like calling an auxiliary function with empty accumulator, to hide the extra parameter from the external interface) Example -- ATS class C a where type T a m :: a-T a instance C Int where type T Int = Int m _ = 1 -- alternative FD encoding attempt class CT a b | a - b instance CT Int Int class CT a b = C a where m :: a- b instance CT Int b = C Int where m _ = 1::b Hm, I haven't thought about this. Two comments. You use scoped variables in class declarations. Are they available in ghc? How do you encode? --AT instance C a = C [a] where type T [a] = [T a] m xs = map m xs Via the following I guess? instance CT a b = CT a [b] instance C a = C [a] where m xs = map m xs It seems your solution won't suffer from the problem I face. See below. -- FD encoding class T a b | a-b instance T Int Int class C a where m :: T a b = a-b instance C Int where m _ = 1 -- general recipe: -- encode type functions T a via type relations T a b -- replace T a via fresh b under the constraint C a b My AT encoding won't work with ghc/hugs because the class declaration of C demands that the output type b is univeral. Though, in the declaration instance C Int we return an Int. Hence, the above cannot be translated to System F. Things would be different if we'd translate to an untyped back-end. referring to the associated type seems slightly awkward in these encodings, so the special syntax for ATS would still be useful, but I agree that an encoding into FDs should be possible. The FD program won't type check under ghc but this doesn't mean that it's not a legal FD program. glad to hear you say that. but is there a consistent version of FDs that allows these things - and if not, is that for lack of trying or because it is known not to work? The FD framework in Understanding FDs via CHRs clearly subsumes ATs (based on my brute-force encoding). My previous email showed that type inference for FDs and ATs can be equally tricky. Though, why ATs? Well, ATs are still *very useful* because they help to structure programs (they avoid redundant parameters). On the other hand, FDs provide the user with the convenience of 'automatic' improvement. Let's do a little test. Who can translate the following FD program to AT? zip2 :: [a]-[b]-[(a,b)] zip2 (a:as) (b:bs) = (a,b) : (zip2 as bs) zip2 _ _ = [] class Zip a b c | c - a, c - b where mzip :: [a] - [b] - c instance Zip a b [(a,b)] where mzip = zip2 instance Zip (a,b) c e = Zip a b ([c]-e) where mzip as bs cs = mzip (zip2 as bs) cs Martin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Associated Type Synonyms question
Stefan Wehr writes: Martin Sulzmann [EMAIL PROTECTED] wrote:: Stefan Wehr writes: [...] Manuel (Chakravarty) and I agree that it should be possible to constrain associated type synonyms in the context of class definitions. Your example shows that this feature is actually needed. I will integrate it into phrac within the next few days. By possible you mean this extension won't break any of the existing ATS inference results? Yes, although we didn't go through all the proofs. You have to be very careful otherwise you'll loose decidability. Do you have something concrete in mind or is this a more general advice? I'm afraid, I think there's a real issue. Here's the AT version of Example 15 from Understanding FDs via CHRs class D a class F a where type T a instance F [a] where type T [a] = [[a]] instance (D (T a), F a) = D [a] ^^^ type function appears in type class Type inference (i.e. constraint solving) for D [a] will not terminate. Roughly, D [[a]] --_instance D (T [a]), F [a]) --_type function D [[a]], F [a] and so on Will this also happen if type functions appear in superclasses? Let's see. Consider class C a class F a where type T a instance F [a] where type T [a] = [[[a]]] class C (T a) = D a ^ type function appears in superclass context instance D [a] = C [[a]] -- satisfies Ross Paterson's Termination Conditions Consider D [a] --_superclassC (T [a]), D [a] --_type function C [[[a]]], D [a] --_instance D [[a]], D [a] and so on My point: - The type functions are obviously terminating, e.g. type T [a] = [[a]] clearly terminates. - It's the devious interaction between instances/superclasss and type function which causes the type class program not to terminate. Is there a possible fix? Here's a guess. For each type definition in the AT case type T t1 = t2 (or improvement rule in the FD case rule T1 t1 a == a=t2 BTW, any sufficient restriction which applies to the FD case can be lifted to the AT case and vice versa!) we demand that the number of constructors in t2 is strictly smaller than the in t1 (plus some of the other usual definitions). Then, type T [a] = [[a]] although terminating, is not legal anymore. Then, there might be some hope to recover termination (I've briefly sketched a proof and termination may indeed hold but I'm not 100% convinced yet). Martin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Associated Type Synonyms question
Martin Sulzmann [EMAIL PROTECTED] wrote:: Stefan Wehr writes: [...] Manuel (Chakravarty) and I agree that it should be possible to constrain associated type synonyms in the context of class definitions. Your example shows that this feature is actually needed. I will integrate it into phrac within the next few days. By possible you mean this extension won't break any of the existing ATS inference results? Yes, although we didn't go through all the proofs. You have to be very careful otherwise you'll loose decidability. Do you have something concrete in mind or is this a more general advice? Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Associated Type Synonyms question
Something more controversial. Why ATS at all? Why not encode them via FDs? Funny you should say that, just when I've been thinking about the same thing. That doesn't mean that ATS aren't a nice way to describe some special cases of FDs, but my feeling is that if ATS can't be encoded in FDs, then there is something wrong with _current_ FD versions that should be fixed. I'd love to hear the experts' opinions about this claim!-) The main argument for ATS is that the extra parameter for the functionally dependend type disappears, but as you say, that should be codeable in FDs. I say should be, because that does not seem to be the case at the moment. My approach for trying the encoding was slightly different from your's, but also ran into trouble with implementations. First, I think you need a per-class association, so your T a b would be specific to C. Second, I'd use a superclass context to model the necessity of providing an associated type, and instance contexts to model the provision of such a type. No big difference, but it seems closer to the intension of ATS: associated types translate into type association constraints. (a lot like calling an auxiliary function with empty accumulator, to hide the extra parameter from the external interface) Example -- ATS class C a where type T a m :: a-T a instance C Int where type T Int = Int m _ = 1 -- alternative FD encoding attempt class CT a b | a - b instance CT Int Int class CT a b = C a where m :: a- b instance CT Int b = C Int where m _ = 1::b -- FD encoding class T a b | a-b instance T Int Int class C a where m :: T a b = a-b instance C Int where m _ = 1 -- general recipe: -- encode type functions T a via type relations T a b -- replace T a via fresh b under the constraint C a b referring to the associated type seems slightly awkward in these encodings, so the special syntax for ATS would still be useful, but I agree that an encoding into FDs should be possible. The FD program won't type check under ghc but this doesn't mean that it's not a legal FD program. glad to hear you say that. but is there a consistent version of FDs that allows these things - and if not, is that for lack of trying or because it is known not to work? Cheers, Claus It's wrong to derive certain conclusions about a language feature by observing the behavior of a particular implementation! Martin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Associated Type Synonyms question
On Fri, Feb 17, 2006 at 01:26:18PM +, Stefan Wehr wrote:
Martin Sulzmann [EMAIL PROTECTED] wrote::
By possible you mean this extension won't break any
of the existing ATS inference results?
Yes, although we didn't go through all the proofs.
You have to be very careful otherwise you'll loose decidability.
The paper doesn't claim a proof of decidability (or principal types),
but conjectures that it will go through.
Apropos of that, I tried translating the non-terminating FD example from
the FD-CHR paper (ex. 6) to associated type synonyms (simplified a bit):
data T a = K a;
class C a where {
type S a;
r :: a - S a;
}
instance C a = C (T a) where {
type S (T a) = T (S a);
r (K x) = K (r x);
}
f b x = if b then r (K x) else x;
Phrac infers
f :: forall a . (S (T a) = a, C a) = Bool - a - T (S a)
The constraint is reducible (ad infinitum), but Phrac defers constraint
reduction until it is forced (as GHC does with ordinary instance
inference). We can try to force it using the MR, by changing the
definition of f to
f = \ b x - if b then r (K x) else x;
For this to be legal, the constraint must be provable. In the
corresponding FD case, this sends GHC down the infinite chain of
reductions, but Phrac just gives up and complains about deferred
constraints being left over after type inference. I don't think this
is right either, as in other cases the constraint will reduce away
to nothing.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Associated Type Synonyms question
Stefan Wehr writes: Niklas Broberg [EMAIL PROTECTED] wrote:: On 2/10/06, Ross Paterson [EMAIL PROTECTED] wrote: On Fri, Feb 10, 2006 at 05:20:47PM +0100, Niklas Broberg wrote: - when looking at the definition of MonadWriter the Monoid constraint is not strictly necessary, and none of the other mtl monads have anything similar. Is it the assumption that this kind of constraint is never really necessary, and thus no support for it is needed for ATS? I think that's right -- it's only needed for the Monad instance for WriterT. But it is a convenience. In any instance of MonadWriter, the w will be a monoid, as there'll be a WriterT in the stack somewhere, so the Monoid constraint just saves people writing general functions with MonadWriter from having to add it. Sure it's a convenience, and thinking about it some more it would seem like that is always the case - it is never crucial to constrain a parameter. But then again, the same applies to the Monad m constraint, we could give the same argument there (all actual instances will be monads, hence...). So my other question still stands, why not allow constraints on associated types as well, as a convenience? Manuel (Chakravarty) and I agree that it should be possible to constrain associated type synonyms in the context of class definitions. Your example shows that this feature is actually needed. I will integrate it into phrac within the next few days. By possible you mean this extension won't break any of the existing ATS inference results? You have to be very careful otherwise you'll loose decidability. Something more controversial. Why ATS at all? Why not encode them via FDs? Example -- ATS class C a where type T a m :: a-T a instance C Int where type T Int = Int m _ = 1 -- FD encoding class T a b | a-b instance T Int Int class C a where m :: T a b = a-b instance C Int where m _ = 1 -- general recipe: -- encode type functions T a via type relations T a b -- replace T a via fresh b under the constraint C a b The FD program won't type check under ghc but this doesn't mean that it's not a legal FD program. It's wrong to derive certain conclusions about a language feature by observing the behavior of a particular implementation! Martin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Associated Type Synonyms question
Niklas Broberg [EMAIL PROTECTED] wrote:: On 2/10/06, Ross Paterson [EMAIL PROTECTED] wrote: On Fri, Feb 10, 2006 at 05:20:47PM +0100, Niklas Broberg wrote: - when looking at the definition of MonadWriter the Monoid constraint is not strictly necessary, and none of the other mtl monads have anything similar. Is it the assumption that this kind of constraint is never really necessary, and thus no support for it is needed for ATS? I think that's right -- it's only needed for the Monad instance for WriterT. But it is a convenience. In any instance of MonadWriter, the w will be a monoid, as there'll be a WriterT in the stack somewhere, so the Monoid constraint just saves people writing general functions with MonadWriter from having to add it. Sure it's a convenience, and thinking about it some more it would seem like that is always the case - it is never crucial to constrain a parameter. But then again, the same applies to the Monad m constraint, we could give the same argument there (all actual instances will be monads, hence...). So my other question still stands, why not allow constraints on associated types as well, as a convenience? Manuel (Chakravarty) and I agree that it should be possible to constrain associated type synonyms in the context of class definitions. Your example shows that this feature is actually needed. I will integrate it into phrac within the next few days. Stefa ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
