[Haskell-cafe] Modifying a product type generically

Michael Orlitzky michael at orlitzky.com
Fri Jan 2 16:47:46 UTC 2015


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.



More information about the Haskell-Cafe mailing list