Re: [Haskell-cafe] Type class for sequences with dependent types

Hi Eugene, with respect to typing your solution is a lot nicer since the type arguments are not just ignored. But apart from that it does not help too much in the below example, since it does not allow me to get rid of the additional constructor (List in your case, IntList in mine) and it still does not give an instance nil of type [a], so I cannot write things like [x] `app` nil. Fortunately, in my actual development, I used another type than list, so I could just redefine the type in the way you proposed. Assuming the type was actually a redefinition of lists, it would look like: data List_ a b where Nil :: List_ a a Cons :: a -> List_ a a -> List_ a a and then I created a type synonym for convenience. type List a = List_ a a However, (for example) showing that List is a Functor fails with a similar error. instance Functor List where ... The good thing is that I do not need such instances at the moment, so it solves my problem for the time being. Thank you, and also Markus, for the replies, Robbert On 01/05/2012 03:04 PM, Eugene Kirpichov wrote:

Will this help?

data List a b where List :: [a] -> List a a

05.01.2012, в 17:12, Robbert Krebbers написал(а):

...

Hello,

in a Haskell development I have to represent paths that have elements of alternating types. GADTs allow me to do this easily:

data AltList :: * -> * -> * where Nil :: AltList a a ICons :: Int -> AltList Int b -> AltList () b UCons :: () -> AltList () b -> AltList Int b

Since I have various kinds of these data structures I defined a type class for common operations on such data structures.

class DepSequence l where nil :: l a a app :: l a b -> l b c -> l a c

The instance for AltList is as follows:

instance DepSequence AltList where nil = Nil Nil `app` k = k ICons i l `app` k = ICons i (l `app` k) UCons i l `app` k = UCons i (l `app` k)

This all works nicely, however, I also want ordinary lists to be an instance of this class too. I tried the following:

type IntListAlt a b = [Int] instance DepSequence IntListAlt where nil = [] app = (++)

But GHC does not like this, it yields:

Type synonym `IntListAlt' should have 2 arguments, but has been given none In the instance declaration for `DepList IntListAlt'

The following alternative works, but it is quite ugly

newtype IntList a b = IntList { getList :: [Int] } instance DepSequence IntList where nil = IntList [] app l k = IntList (getList l ++ getList k)

and also does not give me a nil of type [Int] and an app of type [Int] -> [Int] -> [Int].

Does anyone know whether Haskell allows me to do this in a better way?

Best,

Robbert

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe