各タイプに固有の異型性がありますか？

Question

最近、私は変態を理解しているように感じ始めました。私はa recent answerにそれらについていくつか書きましたが、簡単に言えば、あるタイプの値を再帰的に横断し、そのタイプのパターンマッチがそのタイプの各コンストラクターごとに1つの関数に統一された形で、私はこの点、または上記の鉱山の答えのより長いバージョンの修正を歓迎するが、私はこれを多かれ少なかれ持っていると思うが、それはこの問題の主題ではなく、ちょっとした背景だ。

カタモフィズムに渡す関数が型のコンストラクタに正確に対応し、これらの関数の引数も同様にそれらのコンストラクタの型の型に対応していることがわかりました。別の実装のためにどこに揺れがあるのか​​を見てください。

たとえば、私はちょうどこの愚かなタイプを構成しました。その構造が何を意味するのかという本来の概念はなく、そのための異型性を導き出しました。私は汎用のこのタイプの上に折る定義することができ、他の方法が表示されない：

data X a b f = A Int b 
      | B 
      | C (f a) (X a b f) 
      | D a 

xCata :: (Int -> b -> r) 
     -> r 
     -> (f a -> r -> r) 
     -> (a -> r) 
     -> X a b f 
     -> r 
xCata a b c d v = case v of 
    A i x -> a i x 
    B -> b 
    C f x -> c f (xCata a b c d x) 
    D x -> d x 

私の質問は、すべてのタイプは、（引数の並べ替えまで）独特catamorphismを持っているんですか？あるいは、逆説的な型：異型性が定義されていないタイプ、または2つのはっきりと同等に合理的な異型性が存在するタイプが存在するか？反例がない場合（すなわち、あるタイプの異型性が一意であり、かつ派生的に導出可能である場合）、GHCにこの種の手作業を自動的に行う何らかの類型を派生させることは可能でしょうか？

Answer 1

再帰型に関連した変態は、機械的に導き出すことができます。

あなたが再帰的に定義された型を持ち、複数のコンストラクタを持ち、それぞれが独自のアリティを持つとします。私はOPの例を借ります。

data X a b f = A Int b 
      | B 
      | C (f a) (X a b f) 
      | D a 

その後、我々はすべてをuncurrying、一つで各アリティを強制することにより、同じタイプを書き換えることができます。ユニットタイプ()を追加すると、Arity zero（B）が1になります。

data X a b f = A (Int, b) 
      | B() 
      | C (f a, X a b f) 
      | D a 

その後、我々は代わりに複数のコンストラクタのEitherを利用し、1にコンストラクタの数を減らすことができます。以下では、簡略化のために、Eitherの代わりに+というインフィクスを書きます。用語レベルで

data X a b f = X ((Int, b) +() + (f a, X a b f) + a) 

、我々は、明示的な固定小数点式x = f xを書いて、フォームx = f x where f w = ...として任意の再帰的定義 を書き換えることができます知っています。タイプレベルでは、refectorの再帰型に対して同じメソッド を使用できます。

data X a b f = X (F (X a b f)) -- fixed point equation 
data F a b f w = F ((Int, b) +() + (f a, w) + a) 

ここで、ファンクタインスタンスを自動作成できることに注意してください。

deriving instance Functor (F a b f) 

オリジナルタイプに各再帰参照のみ正位置で発生したため、これが可能です。これが成り立たなければ、F a b fをファンクタではなく、私たちは異型性を持つことができません。

cata :: (F a b f w -> w) -> X a b f -> w 

これはOPのxCataタイプです：次のように

最後に、我々はcataの種類を書き込むことができますか？そうです。我々は、いくつかの型同型写像を適用すればよい。 1としてユニット()、我々は製品a*bとして(a,b)を書くならば、それはこれらの同型写像を覚えておくのは簡単です、ちなみに

1) (a,b) -> c ~= a -> b -> c   (currying) 
2) (a+b) -> c ~= (a -> c, b -> c) 
3)() -> c ~= c 

、および電源b^aなどa->b：私たちは、次の代数法則を使用しています。実際には1) c^(a*b) = (c^a)^b , 2) c^(a+b) = c^a*c^b, 3) c^1 = cになります。とにかく

、唯一

F a b f w -> w 
=~ (def F) 
    ((Int, b) +() + (f a, w) + a) -> w 
=~ (2) 
    ((Int, b) -> w,() -> w, (f a, w) -> w, a -> w) 
=~ (3) 
    ((Int, b) -> w, w, (f a, w) -> w, a -> w) 
=~ (1) 
    (Int -> b -> w, w, f a -> w -> w, a -> w) 

さんは今、完全な形を考えてみましょう、のは、F a b f w -> w一部を書き換えるために始めましょう：（w=rの名前を変更する）確かにある

cata :: (F a b f w -> w) -> X a b f -> w 
    ~= (above) 
     (Int -> b -> w, w, f a -> w -> w, a -> w) -> X a b f -> w 
    ~= (1) 
      (Int -> b -> w) 
     -> w 
     -> (f a -> w -> w) 
     -> (a -> w) 
     -> X a b f 
     -> w 

希望タイプ

xCata :: (Int -> b -> r) 
     -> r 
     -> (f a -> r -> r) 
     -> (a -> r) 
     -> X a b f 
     -> r 

の「標準」実装は

cata g = wrap . fmap (cata g) . unwrap 
    where unwrap (X y) = y 
     wrap y = X y 

であることは、その一般に理解するためにいくつかの努力がかかりますが、これは確かに意図したものです。

---

自動化について：はい、これは少なくとも部分的には自動化できます。 1は

type X a b f = Fix (F a f b) 
data F a b f w = ... -- you can use the actual constructors here 
     deriving Functor 

-- use cata here 

のようなものを書くことができますhackageのパッケージrecursion-schemesがあります。例：

import Data.Functor.Foldable hiding (Nil, Cons) 

data ListF a k = NilF | ConsF a k deriving Functor 
type List a = Fix (ListF a) 

-- helper patterns, so that we can avoid to match the Fix 
-- newtype constructor explicitly  
pattern Nil = Fix NilF 
pattern Cons a as = Fix (ConsF a as) 

-- normal recursion 
sumList1 :: Num a => List a -> a 
sumList1 Nil   = 0 
sumList1 (Cons a as) = a + sumList1 as 

-- with cata 
sumList2 :: forall a. Num a => List a -> a 
sumList2 = cata h 
    where 
    h :: ListF a a -> a 
    h NilF  = 0 
    h (ConsF a s) = a + s 

-- with LambdaCase 
sumList3 :: Num a => List a -> a 
sumList3 = cata $ \case 
    NilF  -> 0 
    ConsF a s -> a + s