3

関数を作成しようとしています

import Language.Reflection
foo : Type -> TT

reflect私は戦術を使ってそれを試しました：

foo = proof
  {
    intro t
    reflect t
  }

tしかし、これは変数自体に反映されます:

*SOQuestion> foo
\t => P Bound (UN "t") (TType (UVar 41)) : Type -> TT
4

1 に答える 1

3

Idris のリフレクションは、純粋に構文上のコンパイル時のみの機能です。それがどのように機能するかを予測するには、Idris がどのようにプログラムをコア言語に変換するかを知る必要があります。重要なのは、Lisp の場合のように、反映された用語を実行時に把握して再構築することができないということです。プログラムのコンパイル方法は次のとおりです。

  1. 内部的に、Idris は type の何かを期待する穴を作成しますType -> TT。
  2. fooこの状態で証明スクリプトを実行します。前提条件なしで開始し、 type の目標を設定しType -> TTます。つまり、 のような項が構築されています?rhs : Type => TT . rhs。構文は、最終的な値が の内部で利用可能になる と?foo : ty => body呼ばれる穴があることを示しています。foobody
  3. このステップintro tでは、引数が である関数を作成します。t : Typeこれは、 のような項があることを意味し?foo_body : TT . \t : Type => foo_bodyます。
  4. 次に、reflect tステップは、右側の項を取得して に変換することにより、現在の穴を埋めTTます。その用語は、実際には関数の引数への参照にすぎないため、変数を取得しますt。reflectは、他のすべての証明スクリプト ステップと同様に、コンパイル時に直接利用できる情報にのみアクセスできます。foo_bodyしたがって、項の反映で埋めた結果tは ですP Bound (UN "t") (TType (UVar (-1)))。

ここでやりたいことを実行できれば、Idris コードの理解とコードの効率的な実行の両方に大きな影響を与えるでしょう。

理解の喪失は、型に基づいて関数の動作について推論するためにパラメトリック性を使用できないことに起因します。すべての関数は事実上、アドホックなポリモーフィックになる可能性があります。これは、int のリストとは異なる文字列のリストで (たとえば) 実行できるためです。

パフォーマンスの低下は、リフレクションを行うのに十分な型情報を表すことから生じます。Idris コードがコンパイルされた後、型情報は残りません (JVM や .NET などのシステムや、コードがアクセスできるランタイム表現が型にある Python などの動的型付けシステムとは異なります)。Idris では、任意のプログラムを含めることができるため、型が非常に大きくなる可能性があります。これは、はるかに多くの情報を維持する必要があり、型レベルで発生する計算も保存して実行時に繰り返す必要があることを意味します。

コンパイル時にさらなる自動証明のために型の構造を検討したい場合は、applyTactic戦術を見てください。その引数は、反映されたコンテキストと目標を受け取り、反映された新しい戦術スクリプトを返す関数でなければなりません。例はData.Vectソースで見ることができます。

つまり、要約すると、イドリスはあなたが望むことをすることはできず、おそらく決してできることはないだろうが、別の方法で進歩を遂げることができるかもしれない.

于 2015-01-26T04:29:36.513 に答える