same function for different data family instances

[kris...@purestyle.se]

Having some problems understanding how/if it's possible to make a function that operates on all different instances of a data family declaration.

Like so, I would want to write a Show instance for XList a. But it is not possible to use a general type a and map it to Char and () as in this case.

Something like 

instance Show (XList a) where

    show XNil = "hej"

    show (XListUnit whatever) = show whatever

will not work. I read somewhere (forgot where, sorry) that to do this, you have to use GADTs. Is this true, and if so why?

The only thing I got working was the following, using different functions for the different XList instances. which is hyper ugly:

{-# LANGUAGE TypeFamilies #-}

data family XList a

data instance XList Char = XCons !Char !(XList Char) | XNil

data instance XList ()   = XListUnit !Int

format' :: XList Char -> String

format' XNil              = "nil"

format' (XCons elem rest) = [elem] ++ ", " ++ format' rest

format'' :: XList () -> String

format'' (XListUnit x) = concat ["()" | _ <- [1..x]]

[Patrik Jansson]

Somwhat simplified: Given a type family (like Silly a in my lecture), a "family of values" of those types (like silly in my Agda lecture) can only be defined using a method in a type class (if at all). 

This is in contrast to GADTs where the (closed) family of datatypes (like Expr a in L11) can support a single definition of a "family of values" like eval.

/Patrik

https://github.com/AFPChalmers15/AFPcourse/blob/master/L11/src/Typed.hs

https://wiki.haskell.org/GHC/Type_families

"Even if type families are defined as toplevel declarations, functions that perform different computations for different family instances still need to be defined as methods of type classes. In particular, the following is not possible:

data family T a

data instance T Int  = A

data instance T Char = B

nonsense :: T a -> Int

nonsense A = 1             -- WRONG: These two equations together...

nonsense B = 2             -- ...will produce a type error.

Given the functionality provided by GADTs (Generalised Algebraic Data Types), it might seem as if a definition, such as the above, should be feasible. However, type families - in contrast to GADTs - are open; i.e., new instances can always be added, possibly in other modules. Supporting pattern matching across different data instances would require a form of extensible case construct."

--
You received this message because you are subscribed to the Google Groups "afp15" group.
To unsubscribe from this group and stop receiving emails from it, send an email to afp15+un...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[kris...@purestyle.se]

So in theory, it would be possible to have some kind of DataFamilyClosed, that can live in one module only, and then this would work?

If so, it feels clearer to me and thank you for the explanation.