[Haskell-cafe] Re: Associated Type Synonyms question

[Claus Reinke]

> 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