Is it possible to derive recursion principles generically?

Question

In Idris, there's some magical machinery to automatically create (dependent) eliminators for user-defined types. I'm wondering if it's possible to do something (perhaps less dependent) with Haskell types. For instance, given

data Foo a = No | Yes a | Perhaps (Foo a)

I want to generate

foo :: b -> (a -> b) -> (b -> b) -> Foo a -> b
foo b _ _ No = b
foo _ f _ (Yes a) = f a
foo b f g (Perhaps c) = g (foo b f g x)

I'm pretty weak on polyvariadic functions and generics, so I could use a bit of help getting started.

Answer 1

Here's a start of doing this using GHC Generics. Adding some code to reassociate the (:+:) would make this nicer. A few more instances are required and this probably has ergonomic problems.

EDIT: Bah, I got lazy and fell back to a data family to get injectivity for my type equality dispatch. This mildly changes the interface. I suspect with enough trickery, and/or using injective type families this can be done without a data family or overlapping instances.

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
module Main where
import Data.Function (fix)
import GHC.Generics

data Foo a = No | Yes | Perhaps (Foo a) | Extra a Int Bool
    deriving (Show, Generic1)

data Bar a = Bar (Maybe a)
    deriving (Show, Generic1)

gcata :: (GCata (f a) (Rep1 f a), Generic1 f) => Alg (f a) (Rep1 f a) r -> f a -> r
gcata f = fix(\w -> gcata' w f . from1)

ex' :: Show a => Foo a -> String
ex' = gcata (("No","Yes"),(\(Rec s) -> "Perhaps ("++s++")", \a i b -> "Extra ("++show a++") ("++show i++") ("++show b++")"))

ex1 = ex' (Perhaps (Perhaps Yes) :: Foo Int)
ex2 = ex' (Perhaps (Perhaps (Extra 'a' 2 True)) :: Foo Char)

ex3 :: Foo a -> Foo a
ex3 = gcata ((No, Yes), (Perhaps . unRec, Extra))

ex4 = gcata (\(K m) -> show m) (Bar (Just 3))

class GCata rec f where
    type Alg (rec :: *) (f :: *) (r :: *) :: *
    gcata' :: (rec -> r) -> Alg rec f r -> f -> r

instance (GCata rec (f p)) => GCata rec (M1 i c f p) where
    type Alg rec (M1 i c f p) r = Alg rec (f p) r
    gcata' w f (M1 x) = gcata' w f x

instance (GCata rec (f p), GCata rec (g p)) => GCata rec ((f :+: g) p) where
    type Alg rec ((f :+: g) p) r = (Alg rec (f p) r, Alg rec (g p) r)
    gcata' w (l,_) (L1 x) = gcata' w l x
    gcata' w (_,r) (R1 x) = gcata' w r x

instance GCata rec (U1 p) where
    type Alg rec (U1 p) r = r
    gcata' _ f U1 = f

instance (Project rec (f p), GCata rec (g p)) => GCata rec ((f :*: g) p) where
    type Alg rec ((f :*: g) p) r = Prj rec (f p) r -> Alg rec (g p) r
    gcata' w f (x :*: y) = gcata' w (f (prj w x)) y

class Project rec f where
    type Prj (rec :: *) (f :: *) (r :: *) :: *
    prj :: (rec -> r) -> f -> Prj rec f r

instance (Project rec (f p)) => Project rec (M1 i c f p) where
    type Prj rec (M1 i c f p) r = Prj rec (f p) r
    prj w (M1 x) = prj w x

instance Project rec (K1 i c p) where
    type Prj rec (K1 i c p) r = c
    prj _ (K1 x) = x

instance (RecIfEq (TEq rec (f p)) rec (f p)) => Project rec (Rec1 f p) where
    type Prj rec (Rec1 f p) r = Tgt (TEq rec (f p)) rec (f p) r
    prj w (Rec1 x) = recIfEq w x

instance Project rec (Par1 p) where
    type Prj rec (Par1 p) r = p
    prj _ (Par1 x) = x

instance GCata rec (K1 i c p) where
    type Alg rec (K1 i c p) r = c -> r
    gcata' _ f (K1 x) = f x

instance GCata rec (Par1 p) where
    type Alg rec (Par1 p) r = p -> r
    gcata' _ f (Par1 x) = f x

instance (Project rec (Rec1 f p)) => GCata rec (Rec1 f p) where
    type Alg rec (Rec1 f p) r = Prj rec (Rec1 f p) r -> r
    gcata' w f = f . prj w 

data HTrue; data HFalse

type family TEq x y where
    TEq x x = HTrue
    TEq x y = HFalse

class RecIfEq b rec t where
    data Tgt b rec t r :: *
    recIfEq :: (rec -> r) -> t -> Tgt b rec t r

instance RecIfEq HTrue rec rec where
    newtype Tgt HTrue rec rec r = Rec { unRec :: r }
    recIfEq w = Rec . w

instance RecIfEq HFalse rec t where
    newtype Tgt HFalse rec t r = K { unK :: t }
    recIfEq _ = K