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