10

たとえば、Idris の関数で型を返すことができます。

t : Type -> Type -> Type
t a b = a -> b

->しかし、タイプのリストを折り畳むために使用したい状況が発生しました（いくつかのパーサーを作成して実験したとき） 、つまり

typeFold : List Type -> Type
typeFold = foldr1 (->)

だからそれtypeFold [String, Int]は与えるだろうString -> Int : Type. ただし、これはコンパイルされません。

error: no implicit arguments allowed
    here, expected: ")",
    dependent type signature,
    expression, name
typeFold = foldr1 (->)
                   ^

しかし、これはうまくいきます：

t : Type -> Type -> Type
t a b = a -> b

typeFold : List Type -> Type
typeFold = foldr1 t

を使用するためのより良い方法はあり->ますか?そうでない場合は、機能要求として提起する価値がありますか?

4

2 に答える 2

10

この方法で使用->する際の問題は、それが型コンストラクターではなくバインダーであり、ドメインにバインドされた名前が範囲のスコープ内にあるため、それ->自体が直接型を持たないことです。tたとえば、の定義は、のような依存型をキャプチャしません(x : Nat) -> P x。

少し面倒ですが、あなたがしていることはこれを行う正しい方法です。型コンストラクターとして特別な構文を作成する必要があるとは確信してい(->)ません.1つは、実際にはそうではないため、また、依存型で機能しない場合に混乱を招くように感じるためです。

于 2014-12-03T12:29:54.477 に答える
1

このモジュールは、 「newtype」Data.Morphismsの周りのすべてのラッピング/アンラッピングを行う必要があることを除いて、このようなものを提供します。Morphism

于 2016-12-26T22:34:52.553 に答える