是否有可能通常推导出递归原理？

Question

在Idris中,有一些神奇的机器可以自动为用户定义的类型创建(依赖)消除器.我想知道是否可以使用Haskell类型做一些事情(可能更少依赖).例如,给定

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

我想生成

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)

我对多变量函数和泛型非常弱,所以我可以使用一些帮助入门.

Answer 1

以下是使用GHC Generics进行此操作的开始.添加一些代码来重新关联(:+:)会使这更好.需要更多实例,这可能存在人体工程学问题.

编辑:呸,我懒得回到数据系列,以获得我的类型平等派遣的注入性.这温和地改变了界面.我怀疑有足够的诡计,和/或使用内射类型系列,这可以在没有数据族或重叠实例的情况下完成.

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

Answer 2

作为pigworker在问题的评论说,使用默认的Generic表示导致大丑,因为我们没有对我们的类型递归先验信息,我们必须通过平等型手动检查挖出递归发生.我想在这里介绍具有显式f-algebra风格递归的替代解决方案.为此,我们需要一个替代的通用Rep.可悲的是,这意味着我们不能轻易进入GHC.Generics,但我希望这仍然会有所启发.

在我的第一个解决方案中,我的目标是在当前的GHC功能中尽可能简单地进行演示.第二种解决方案是TypeApplication基于GHC 8 的重型解决方案,具有更复杂的类型.

像往常一样开始:

{-# language
  TypeOperators, DataKinds, PolyKinds,
  RankNTypes, EmptyCase, ScopedTypeVariables,
  DeriveFunctor, StandaloneDeriving, GADTs,
  TypeFamilies, FlexibleContexts, FlexibleInstances #-}

我的通用表示是产品总和的固定点.它稍微扩展了基本模型generics-sop,它也是产品的总和,但不是函数,因此不适合递归算法.我认为SOP总体上比任意嵌套类型更好的实际表示; 你可以找到扩展的论据,为什么在本文中就是这种情况.简而言之,SOP删除了不必要的嵌套信息,并允许我们将元数据与基本数据分开.

但在此之前,我们应该决定泛型类型的代码.在vanilla GHC.Generics中没有明确定义的代码类型,因为sums,products等的类型构造函数构成了一种特殊的类型级语法,我们可以使用类型类对它们进行调度.我们更依赖于依赖类型泛型中的常规表示,并使用显式代码,解释和函数.我们的代码应该是善良的:

[[Maybe *]]

外部列表对构造函数的总和进行编码,每个内部[Maybe *]编码构造函数.A Just *只是一个构造函数字段,而Nothing表示递归字段.例如,代码[Int]是['[], [Just Int, Nothing]].

type Rep a = Fix (SOP (Code a)) 

class Generic a where
  type Code a :: [[Maybe *]]
  to   :: a -> Rep a
  from :: Rep a -> a

data NP (ts :: [Maybe *]) (k :: *) where
  Nil  :: NP '[] k
  (:>) :: t -> NP ts k -> NP (Just t ': ts) k
  Rec  :: k -> NP ts k -> NP (Nothing ': ts) k
infixr 5 :>  

data SOP (code :: [[Maybe *]]) (k :: *) where
  Z :: NP ts k -> SOP (ts ': code) k
  S :: SOP code k -> SOP (ts ': code) k

请注意,NP递归和非递归字段具有不同的构造函数.这非常重要,因为我们希望代码明确地反映在类型索引中.换句话说,我们也想NP扮演一个单身人士[Maybe *](虽然我们仍然*有充分理由保持参数化).

我们k在定义中使用一个参数为递归留下一个漏洞.我们像往常一样设置递归,将Functor实例留给GHC:

deriving instance Functor (SOP code)
deriving instance Functor (NP code)

newtype Fix f = In {out :: f (Fix f)}

cata :: Functor f => (f a -> a) -> Fix f -> a
cata phi = go where go = phi . fmap go . out

我们有两个类型系列:

type family CurryNP (ts :: [Maybe *]) (r :: *) :: * where
  CurryNP '[]             r = r
  CurryNP (Just t  ': ts) r = t -> CurryNP ts r
  CurryNP (Nothing ': ts) r = r -> CurryNP ts r

type family Alg (code :: [[Maybe *]]) (r :: *) :: * where
  Alg '[]         r = ()
  Alg (ts ': tss) r = (CurryNP ts r, Alg tss r)

CurryNP ts rNP ts与结果类型的curries r,它也插入r递归事件.

Alg code r计算代数的类型SOP code r.它将各个构造函数的消除器组合在一起.这里我们使用普通的嵌套元组,但当然HList-s也足够了.我们也可以NP在这里重复使用HList,但我发现它过于笨拙.

剩下的就是实现这些功能:

uncurryNP :: CurryNP ts a -> NP ts a -> a
uncurryNP f Nil        = f
uncurryNP f (x :> xs)  = uncurryNP (f x) xs
uncurryNP f (Rec k xs) = uncurryNP (f k) xs

algSOP :: Alg code a -> SOP code a -> a
algSOP fs (Z np)  = uncurryNP (fst fs) np
algSOP fs (S sop) = algSOP (snd fs) sop

gcata :: Generic a => Alg (Code a) r -> a -> r
gcata f = cata (algSOP f) . to

这里的关键点是我们必须将咖喱消除器Alg转换为"适当的" SOP code a -> a代数,因为这是可以直接使用的形式cata.

让我们定义一些糖和实例:

(<:) :: a -> b -> (a, b)
(<:) = (,)
infixr 5 <:

instance Generic (Fix (SOP code)) where
  type Code (Fix (SOP code)) = code
  to   = id
  from = id  

instance Generic [a] where
  type Code [a] = ['[], [Just a, Nothing]]  
  to   = foldr (\x xs -> In (S (Z (x :> Rec xs Nil)))) (In (Z Nil))
  from = gcata ([] <: (:) <: ()) -- note the use of "Generic (Rep [a])"

例:

> gcata (0 <: (+) <: ()) [0..10]
55

完整代码.

但是,如果我们进行了调整并且不必使用HList-s或元组来存储消除器,那就更好了.最方便的方法是使用与标准库折叠中相同的参数顺序,例如foldr或maybe.在这种情况下,返回类型gcata由类型族给出,该类型族从类型的通用代码计算.

type family CurryNP (ts :: [Maybe *]) (r :: *) :: * where
  CurryNP '[]             r = r
  CurryNP (Just t  ': ts) r = t -> CurryNP ts r
  CurryNP (Nothing ': ts) r = r -> CurryNP ts r

type family Fold' code a r where
  Fold' '[]         a r = r
  Fold' (ts ': tss) a r = CurryNP ts a -> Fold' tss a r

type Fold a r = Fold' (Code a) r (a -> r)

gcata :: forall a r. Generic a => Fold a r

这gcata是高度(完全)模棱两可的.我们需要明确的应用,或者Proxy我选择前者,引起GHC 8的依赖.但是,一旦我们提供了a类型,结果类型就会减少,我们可以轻松地进行调整:

> :t gcata @[_] 
gcata @[_] :: Generic [t] => r -> (t -> r -> r) -> [t] -> r
> :t gcata @[_] 0
gcata @[_] 0 :: Num t1 => (t -> t1 -> t1) -> [t] -> t1
> gcata @[_] 0 (+) [0..10]
55

我在上面使用了部分类型签名[_].我们还可以为此创建一个简写:

gcata1 :: forall f a r. Generic (f a) => Fold (f a) r
gcata1 = gcata @(f a) @r

哪个可以用作gcata1 @[].

我不想在gcata这里详细说明上面的实现.它不比简单版本长,但gcata实现非常毛茸茸(令人尴尬的是,它是我的延迟答案的原因).现在我无法解释它,因为我用Agda援助写了它,这需要大量的自动搜索和类型俄罗斯方块.