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

• 門脇, 香子

• 浅井, 健一

書誌事項

タイトル別名

• Type Inference in Agda

抄録

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.

収録刊行物

• 第56回プログラミング･シンポジウム予稿集

  第56回プログラミング･シンポジウム予稿集 2015 115-120, 2015-01-09

キーワード

• Agda, Type Inference, Proof Theory

詳細情報

• CRID: 1050855522086396416
• NII論文ID: 170000151297
• Web Site: http://id.nii.ac.jp/1001/00146658/
• 本文言語コード: ja
• 資料種別: conference paper
• データソース種別:
  • IRDB
  • CiNii Articles
  • KAKEN