一般的に再帰の原則を導き出すことは可能ですか？

Question

Idrisには、ユーザー定義型のエリミネーターを自動的に（依存して）作成するいくつかの魔法の仕組みがあります。ハスケル型で何か（おそらくあまり依存しない）をすることが可能かどうか疑問に思っています。例えば、私は

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) 

を生成したい

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

与えられた私はpolyvariadic機能やジェネリック医薬品のかなり弱いので、私は始める助けのビットを使用することができます。

Answer 1

ここでは、GHC Genericsを使用してこれを開始します。 (:+:)を再関連付けするためのコードを追加すると、これはより良いものになります。いくつかのインスタンスが必要となり、おそらく人間工学的な問題があります。

編集：：私は怠け者になり、私の型平等ディスパッチのための注射能力を得るためにデータファミリーに落ちました。これによりインターフェイスが穏やかに変わります。私は十分なtrickeryと思っていますが、注入型のファミリを使用すると、データファミリや重複するインスタンスがなくても実行できます。

{-# 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-styleの再帰的な明示的な代替解を提示したいと思います。このためには代替の汎用Repが必要です。残念ながら、これは容易にGHC.Genericsに入ることができないことを意味しますが、それでもそれが啓発されることを願っています。

私の最初の解決策では、現在のGHC機能の中でできるだけシンプルなプレゼンテーションを目指しています。 2つ目の解決策は、より洗練されたタイプの、重いGHC 8ベースのものであるTypeApplicationです。

いつものように出始め：

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

私の一般的な表現は、積和の不動点です。 generics-sopの基本モデルをわずかに拡張していますが、これも製品の合計ですが、ファンクションではないため、再帰的なアルゴリズムには不備があります。私はSOPが全体的に任意のネストされた型よりはるかに実用的な表現だと思う。なぜこれがpaperの場合に該当するかについての拡張引数を見つけることができます。要するに、SOPは不要なネスト情報を削除し、基本データからメタデータを分離することができます。

しかし、何よりも前に、ジェネリック型のコードを決定する必要があります。バニラのGHC.Genericsでは、総和、型などの型コンストラクタがアドホック型レベルの文法を形成するため、明確な種類のコードはなく、型クラスを使用してそれらをディスパッチすることができます。私たちは、依存型ジェネリックの通常のプレゼンテーションにもっと忠実に従い、明示的なコード、解釈、関数を使用します。我々のコードは、種類のものでなければならない：

[[Maybe *]] 

外側のリストには、各内側[Maybe *]コンストラクタをコードする、コンストラクタの和を符号化します。 Just *はコンストラクタフィールドに過ぎず、Nothingは再帰フィールドを表します。たとえば、[Int]のコードは['[], [Just Int, Nothing]]です。NPは再帰と非再帰的なフィールドのさまざまなコンストラクタを持っていることを

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は[Maybe *]のシングルトンとしても機能したいと考えています（しかし、良い理由から私たちは*にパラメトリックになっています）。

定義内にkパラメータを使用して、再帰のための穴を残します。

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 

我々は2種類のファミリがあります：私たちは、GHCにFunctorインスタンスを残して、いつものように再帰を設定

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 rカレーNP ts結果タイプ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 

それはその可能な形式であるため、ここでのキーポイントは、私たちが「正しい」SOP code a -> a代数にAlgでカリーエリミネーターを変換しなければならないことです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 

Full code.

---

我々はカリー化していたし、持っていなかった場合は、それがよりよいだろう削除ツールを格納するために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 @[]として使用することができます

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

：我々はまた、このための速記を作成することができます。

ここではimplementation of the above gcataを詳しく説明しません。それは単純なバージョンよりはるかに長くはありませんが、gcata実装はかなり毛深いです（恥ずかしがらず、私の遅れた回答を担当しています）。今私はそれを非常にうまく説明できませんでした。なぜなら、私はAgdaの助けを借りてそれを書いたからです。それは、たくさんの自動検索とタイプのテトリスを必要とします。

Answer 3

コメントやその他の回答で述べたように、再帰的な位置にアクセスできる汎用表現から始めるのが最善です。そのような表現で動作

のライブラリは、（別のcompdataである）multirecある：

{-# LANGUAGE TemplateHaskell #-} 
{-# LANGUAGE GADTs, TypeFamilies, MultiParamTypeClasses, RankNTypes #-} 
module FooFold where 

import Generics.MultiRec.FoldAlgK 
import Generics.MultiRec.TH 

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

data FooF :: * -> * -> * where 
    Foo :: FooF a (Foo a) 

deriveAll ''FooF 

foldFoo :: (r, (a -> r, r -> r)) -> Foo a -> r 
foldFoo phi = fold (const phi) Foo 

FoldAlgKモジュールは、単一の結果タイプの折り目を提供し、ネストされた一対のような代数式を計算します。それをさらにカレーすることは比較的容易であろう。ライブラリによって提供されるいくつかの変形があります。