School of Computing

A Type Theory with Partially Defined Functions

Yong Luo

Technical Report 10-05, University of Kent, Computing Laboratory, University of Kent, Canterbury, Kent, UK, October 2005.

Abstract

Only can totally defined functions be introduced in conventional dependently typed systems and such functions are normally defined by eliminators. Because of the limitation of the elimination rules, many (mathematical) functions cannot be defined in these systems. This paper argues that the restriction of totality is unnecessary, and proposes a type theory that allows partially defined functions. In this type theory, functions can be introduced by means of pattern matching. It is in general undecidable in dependently typed systems whether patterns cover all the canonical objects of a type, and it is one of the big problems for implementation. Without the restriction of totality, we don't have such problem of totality checking, and hence we have more flexibility to introduce functions than we do in conventional type systems.

Download publication 381 kbytes (PDF)

Bibtex Record

@techreport{2270,
author = {Yong Luo},
title = {{A Type Theory with Partially Defined Functions}},
month = {October},
year = {2005},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2005/2270},
    publication_type = {techreport},
    submission_id = {1347_1131095221},
    number = {10-05},
    address = {University of Kent, Canterbury, Kent, UK},
    institution = {University of Kent, Computing Laboratory},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014