3

Idris で次のような関数を作成しようとしました。

strSplit : String -> Maybe (Char, String)

Charこれは、文字列を最初の文字列と残りの文字列に「un-cons」し、Nothing空の場合は戻ります。

だから私はこれを書きましたが、失敗しました：

strSplit x = case strM of
    StrNil       => Nothing
    StrCons c cd => Just (c, cs)

それで、私はこれを試しましたPrelude.Strings。

strSplit x with (strM x)
    strSplit ""             | StrNil         = Nothing
    strSplit (strCons c cs) | (StrCons c cs) = Just (c, cs)

これは問題なくコンパイルおよび実行されました。

私の質問は、なぜwithこのように文字列を分割するためにその規則を使用しなければならないのですか? また、元の方法が失敗するのはなぜですか?

注: 申し訳ありませんが、現時点ではインタープリターにアクセスできないため、エラー メッセージをここに書き込むことはまだできません。

4

1 に答える 1

4

ここには 2 つの問題があります。まず、'case' ブロックでは、引数は'with' ブロックの場合とは異なり、さまざまstrMなstrM xことを調べています。

ただし、もっと興味深い問題があります。最初の問題を修正しようとすると、次のようになります。

strSplit : String -> Maybe (Char, String)
strSplit x = case strM x of
    StrNil       => Nothing
    StrCons c cd => Just (c, cs)

別のエラーが発生します (これは、エラー メッセージを書き換えた現在のマスターからのものです)。

Type mismatch between
    StrM "" (Type of StrNil)
and
    StrM x (Expected type)

したがって、'case' と 'with' の違いは、'with' は、調べているものが左側の型と値に影響を与える可能性があることを考慮していることです。「case」では、一致する strM x は xが "" でなければならないことを意味しますが、「case」はどこにでも出現でき、他の引数の型への影響を考慮しません (これに対する適切な型チェック規則を作成することは、かなりの挑戦…）。

一方、'with' はトップ レベルでのみ表示されます。事実上、それが行っていることは、他のパターンの型と値に影響を与えることができる別のトップ レベルのものを追加することです。

したがって、簡単な答えは、'with' は従属パターン マッチングをサポートしますが、'case' はサポートしないということです。

于 2015-06-02T08:06:30.610 に答える