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