7

次のように、型が関数型かどうかを判断する関数が必要です。

isFunction : Type -> Bool
isFunction (a -> b) = True
isFunction _ = False

Trueただし、これはすべての入力に対して返されます。どうすればこれを機能させることができますか？

4

2 に答える 2

8

Type でのマッチングは、type-casesと呼ばれます。これを行うことができれば、非常に価値のあるパラメトリック性と呼ばれる概念が崩れます。

https://stackoverflow.com/a/23224110/108359

Idris は型のケース化をサポートしていません。ある段階では試みたかもしれないと思いますが、人々はすぐにあきらめました。また、型の大文字と小文字を区別しようとしたときにエラーが発生していましたが、チェックによってバグが発生したため、現在は無効になっています。

エラーは発生しなくなりましたが、またはType -> Boolとは異なる動作をする の実装を提供することはできません。const Trueconst False

申し訳ありませんが、この機能は使用できません。制限のように聞こえるかもしれませんが、これに似た機能を求める動機があると考えるたびに、代わりにもっと明示的な方法でプログラムを構成できたはずだと最終的に考えました。

于 2015-01-04T05:00:02.210 に答える
1

ここでの質問は次のとおりです。なぜこのようなものが必要なのですか?

任意の Idris 型が関数かどうかを調べる必要がありますか? それとも、イドリス タイプの特定のサブセットからこれを見つける必要があるだけですか? 最初のものの可能なアプリケーションを理解することはできませんが、必要な2番目のものである場合は、次のように、これらの型の値を処理するための独自の埋め込み言語を定義できます:

data Ty = TyNat | TyString | TyFun Ty Ty | ...

isFunction : Ty -> Bool
isFunction (TyFun _ _) = True
isFunction _ = False

この種の埋め込み言語を実装する方法の詳細については、この講演をご覧ください: https://vimeo.com/61663317

于 2015-04-20T05:21:04.140 に答える