[Haskell-cafe] Re: Associated Type Synonyms question

[Martin Sulzmann]

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