Type Inference in Agda

IPSJ

Bibliographic Information

Other Title
  • Agdaによる型推論器の定式化

Description

Agda はマルティンレフの型理論に基づいた定理証明支援器であり,その一方で依存型をもつ関数型プログラミング言語でもある.Agda では依存型 (Dependant Types) を用いることができるのも大きな特徴である.また,定理証明支援器とプログラミング言語両方の特徴をもちあわせていることから,何かを実装しつつ証明するのに適している.そこで本稿では,停止性が保証された型推論器を Agda により構成する.なかでも, Unification の実装では, McBride の手法を採用する.これは型変数の数を巧妙に管理することで構造に従った再帰を使って(つまり停止性が明らかな形で)型の Unification を表現できることを示したものである.本稿では Term の型変数の数に注目しつつ,主に Unification の部分と Application の実装にフォーカスを当てながら実装していく.

Agda is a dependently typed functional programming language based on Zhaohui Luo's UTT a type theory similar to Martin-L‡f type theory. Agda is also based on dependent type theory.This paper used Agda to implement a Type inference guaranteed to avoid compose non-stopping program by a structural recursion of McBride's technique. This paper focused number of typing variables, Unification and implementation of application data constructor.

Journal

Related Projects

See more

Keywords

Details 詳細情報について

Report a problem

Back to top