型レベル関数を持つプログラミング言語

そこには、それが提供するのと同じセットを可能にするプログラミング言語はありますか?タイプレベルでも同様に使用できますか?私は、Haskellと他のいくつかのMLファミリ言語ではパラメトリック型が許されていますが、これらは通常非常に限定されており、新しい型を定義するための非常に特殊な構文を持っています。

明確にするために、次の擬似コードを想像してください:

person = { name: 'jon', lastName: 'doe', age: 600 }
assoc = (k, v, obj) => 
   returns { name: 'jon', lastName: 'doe', age: 600, k: v }

assoc('color', 'red', person)
  //evaluates to { name: 'jon', lastName: 'doe', age: 600, color: 'red' }

したがって、これは価値水準にあります。しかし、私はタイプ・レベルで同じことをするための言語を探しています:

type Person = { name: String, lastName: String, age: Int }
type Color = Red | Yellow

assoc = (k, v, type) => 
   returns a new type { name: String, lastName: String, age: Int, k: v }

assoc(color, Color, Person)
  //evaluates to { name: String, lastName: String, age: Int, color: Color }

あなたはポイントを得る、そう?基本的に、PLがあなたが値に対して行うことを可能にするものは、型でも行うことができます。これは、型を値として扱います。

ベストアンサー

はい、これはあなたが思っていたよりはるかに一般的です。 C +
+で意味のある(そして実際にはTuring-complete!)タイプレベルの計算を行うことができます(このMatt
Mattの投稿
)ハスケルは、タイプファミリなどを介して型レベルの部分的な関数を許可します。

もちろん、あなたの記述に最もよく合うシステムは、おそらくタイプと用語を統一する依存型定義です。つまり、依存型言語での型レベルと値レベルの計算は区別されません。無数の依存型システム(Calculus
of Constructions、Martin-Lof型理論、Zhaohui
LuoのUTTなど)、依存型プログラミング言語(Coq、Agda、Idris、あなたはそれを挙げている)がたくさんあります。

だから、私はこの質問がどこの研究レベルにあるのか疑問だ。しかし、あなたの質問への答えは、はい、そのような言語があり、たくさんあり、そのような言語の理論はすでにかなりよく研究されています。依存型に関する参考文献については、Benjamin
Pierceらのタイプとプログラミング言語の高度なトピック(ATTAPL)の第2章またはソフトウェアの基礎を参照してください。
Edwin Bradyの Idrisを使ったタイプ駆動開発で、コードを扱う傾向がある方はぜひ。

返信を残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です