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

[Eugene Kirpichov]

Will this help?

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

05.01.2012, в 17:12, Robbert Krebbers <mailinglists at robbertkrebbers.nl> написал(а):

> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe