[Haskell-cafe] Type arithmetic with ATs/TFs

[Ryan Ingram]

Actually, at least in GHC, associated types are just syntax sugar for
type families.

That is, this code:

class Container c where
   type Element c :: *
   view :: c -> Maybe (Element c,c)

instance Container [a] where
   type Element [a] = a
   view [] = Nothing
   view (x:xs) = Just (x,xs)

is the same as this code:

type family Element c :: *
class Container c where
   view :: c -> Maybe (Element c, c)
type instance Container [a] = a
instance Container [a] where
   view [] = Nothing
   view (x:xs) = Just (x,xs)

  -- ryan

On Thu, Feb 11, 2010 at 1:10 PM, Andrew Coppin
<andrewcoppin at btinternet.com> wrote:
> Andrew Coppin wrote:
>>
>> OK, so I sat down today and tried this, but I can't figure out how.
>>
>> There are various examples of type-level arithmetic around the place. For
>> example,
>>
>> http://www.haskell.org/haskellwiki/Type_arithmetic
>>
>> (This is THE first hit on Google, by the way. Haskell is apparently THAT
>> popular!) But this does type arithmetic using functional dependencies; what
>> I'm trying to figure out is how to do that with associated types.
>>
>> Any hints?
>
> Several people have now replied to this, both on and off-list. But all the
> replies use type families, not associated types.
>
> Now type families are something I don't yet comprehend. (Perhaps the replies
> will help... I haven't studied them yet.) What I understand is that ATs
> allow you to write things like
>
>  class Container c where
>   type Element c :: *
>   ...
>
> And now you can explicitly talk about the kind of element a container can
> hold, rather than relying on the type constructor having a particular kind
> or something. So the above works for containers that can hold *anything*
> (such as lists), containers which can only hold *one* thing (e.g.,
> ByteString), and containers which can hold only certain things (e.g., Set).
>
> ...which is great. But I can't see a way to use this for type arithmetic.
> Possibly because I don't have a dramatically solid mental model of exactly
> how it works. You'd *think* that something like
>
>  class Add x y where
>   type Sum x y :: *
>
>  instance Add x y => Add (Succ x) y where
>   type Sum (Succ x) y = Succ (Sum x y)
>
> ought to work, but apparently not.
>
> As to what type families - type declarations outside of a class - end up
> meaning, I haven't the vaguest idea. The Wiki page makes it sound
> increadibly complicated...
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>