Type class for sequences with dependent types

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

Hi
This has been discussed here[1] and here[2], and the answer is that
its not possible because of making type inference generally
impossible. It would be a useful feature though, and could be
implemented by requiring the user give additional type signatures to
help the inference algorithm out. But that is AFAIK not implemented
yet.
[1] http://www.haskell.org/pipermail/haskell-cafe/2011-July/093790.html
[2] http://comments.gmane.org/gmane.comp.lang.haskell.glasgow.user/21017
On Thu, Jan 5, 2012 at 3:12 PM, 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
-- Markus Läll

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

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
participants (3)
-
Eugene Kirpichov
-
Markus Läll
-
Robbert Krebbers