[Haskell-cafe] Re: Associated Type Synonyms question
Martin Sulzmann
sulzmann at comp.nus.edu.sg
Tue Feb 21 03:00:12 EST 2006
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
More information about the Haskell-Cafe
mailing list