7

私は自分のプログラムで実存的なタイプに苦労しています。私は非常に合理的なことをしようとしていると思いますが、タイプチェッカーを乗り越えることはできません:(

モナドを模倣したデータ型があります

data M o = R o | forall o1. B (o1 -> M o) (M o1)

ここで、 Zipperに関するHaskell Wikiの記事で説明されているものと同様のコンテキストを作成しますが、簡単にするためにデータ構造の代わりに関数を使用します-

type C o1 o2 = M o1 -> M o2

データ値をコンテキストとサブ値に分割する関数を作成しようとすると、タイプチェッカーは次のように文句を言います。

ctx :: M o -> (M o1 -> M o, M o1)
ctx (B f m) = (B f, m) -- Doesn't typecheck

エラーは-

Couldn't match type `o2' with `o1'
  `o2' is a rigid type variable bound by
       a pattern with constructor
         B :: forall o o1. (o1 -> M o) -> M o1 -> M o,
       in an equation for `ctx'
       at delme1.hs:6:6
  `o1' is a rigid type variable bound by
       the type signature for ctx :: M o -> (M o1 -> M o, M o1)
       at delme1.hs:6:1
Expected type: M o2
  Actual type: M o1
In the expression: m
In the expression: (B f, m)

しかし、私はそのようにそれを回避することができます-

ctx (B f m) = let (c,m') = ctx m in ((B f) . c, m') -- OK

なぜこの2番目の定義はタイプチェックするのに、最初の定義はタイプチェックしないのですか？

また、Rをチェックして完全な関数に変換しようとするctxと、タイプチェックエラーが再び発生します-

ctx (R o) = (id, R o) -- Doesn't typecheck

エラー -

Couldn't match type `o' with `o1'
  `o' is a rigid type variable bound by
      the type signature for ctx :: M o -> (M o1 -> M o, M o1)
      at delme1.hs:7:1
  `o1' is a rigid type variable bound by
       the type signature for ctx :: M o -> (M o1 -> M o, M o1)
       at delme1.hs:7:1
In the first argument of `R', namely `o'
In the expression: R o
In the expression: (id, R o)

このエラーを回避するにはどうすればよいですか？

どんな助けでも大歓迎です！

4

1 に答える 1

9

最初に失敗したケースを見てみましょう。これらは両方とも同じ理由で失敗します。これはforall、型シグネチャに暗黙的に追加するとより明確になります。

ctx :: forall o o1. M o -> (M o1 -> M o, M o1)

つまり、関数は一部の関数だけo1でなく、任意 o1の関数でも機能する必要があります。

  1. 最初のケースでは、

    ctx (B f m) = (B f, m)

    私たちはそれを知っています、f :: (o2 -> M o)そしてm :: M o2、いくつかのタイプについては、私たちはどんなタイプもo2提供できなければならないので、それを仮定することはできません。o1o1 ~ o2

  2. 2番目のケースでは、

    ctx (R o) = (id, R o)

    ここでは、を知っていo :: oますが、ここでも、関数は任意 o1のに対して定義する必要があるため、それを想定することはできませんo ~ o1。

帰納法の証明と同様に、回避策はそれ自体を呼び出しているためにのみ機能するようです。ただし、基本ケースがないと、循環論法になり、この関数の基本ケースを記述できません。これは、ボトム値を使用せずに、の任意の組み合わせに対してM o1からを作成する方法がないためです。M ooo1

おそらく行う必要があるのは、タプルだけを使用するのではなく、コンテキストに別の実存型を定義することです。それがあなたのニーズに合うかどうかはわかりませんが、これは少なくとも1をコンパイルします：

data Ctx o = forall o1. Ctx (M o1 -> M o) (M o1)

ctx :: M o -> Ctx o
ctx (B f m) = case ctx m of Ctx c m' -> Ctx (B f . c) m'
ctx (R o)   = Ctx id (R o)

1面白いGHCエラーletの代わりにをcase使用してみてください:)

于 2011-11-25T21:53:40.080 に答える