same function for different data family instances

28 views
Skip to first unread message

kris...@purestyle.se

unread,
Mar 4, 2015, 3:05:55 PM3/4/15
to af...@googlegroups.com
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

unread,
Mar 4, 2015, 4:42:34 PM3/4/15
to af...@googlegroups.com
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




"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

unread,
Mar 5, 2015, 3:10:41 PM3/5/15
to af...@googlegroups.com
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.
Reply all
Reply to author
Forward
0 new messages