
On 01/02/2015 04:22 AM, Roman Cheplyaka wrote:
The absent case corresponds to a multi-constructor type. You need to decide what to do in that case.
You can decide not to allow it, in which case you can enforce it by saying
(xss ~ '[x], yss ~ '[a ': x])
(essentially replacing xs with '[]).
Or perhaps you do want to handle those cases; then it depends on how exactly you want to map multiple constructors.
Thanks, this is so cool. Like, I'm eight years old with a working machine gun cool. First, I got it working with your type signature above. That really helped me understand what was going on, but GHC still warned me about the missing case, and I didn't want to "error" it. I see now that `xss` and `yss` are type-level lists-of-lists, and that there's more than one element in that list if we have more than one constructor. If I want to prepend a new type to the list for both cases, I need something better than [a ': x], which only appends the type `a` to the FIRST (only) list in the list-of-lists. Unfortunately, there are no sections for type operators yet =) So this doesn't work: Map (a ':) xs. But the following recursive definition does: type family Prepended a (xs :: [k]) :: [l] type instance Prepended a '[] = '[] type instance Prepended a (x ': xs) = (a ': x) ': (Prepended a xs) The dubious second line makes sense when you realize that we're working on lists-of-lists, and prepending to the INNER lists. Now the type of `yss` is obvious. In fact, we don't need `yss` any more: prepend_sop :: a -> SOP I xss -> SOP I (Prepended a xss) The first case is the same: prepend_sop z (SOP (Z rest)) = SOP $ Z ((I z) :* rest) But the second one I can define recursively: prepend_sop z (SOP (S rest)) = let (SOP result) = prepend_sop z (SOP rest) in SOP $ S $ result The definition of `prepend` is the same, albeit with a new type. And, holy shit, it works. If I give Foo and BigFoo additional constructors, data Foo = Foo Int Int | Bar Int Int deriving (Show, GHC.Generic) instance Generic Foo data BigFoo = BigFoo String Int Int | BigBar String Int Int deriving (Show, GHC.Generic) instance Generic BigFoo then the `prepend` function knows which one to choose based on the constructor!
prepend "Hello" (Foo 1 2) :: BigFoo BigFoo "Hello" 1 2
prepend "Hello" (Bar 1 2) :: BigFoo BigBar "Hello" 1 2
Awesome.