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

[Robbert Krebbers]

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<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