partial (and non deterministic) functions in dependently typed lambda calculus

Question

A partial function is one, that that is only defined on a part of its domain. Haskell gives examples: https://wiki.haskell.org/Partial_functions

My end goal is to express types

$$ \prod_{D:\mathcal{U}} D \qquad\qquad\qquad\qquad \prod_{\mathcal{A}:\mathfrak{A}} \mathcal{L}(\mathcal{A}) $$

• The first type should simply represent sort of (polymorphic) choice functions which accecpt a type and return an element of that Type.
• The second is assuming, that I can express the Type of Automata $\mathfrak{A}$ as well as the language $\mathcal{L}(\mathcal{A})$ accepted by automaton $\mathcal{A}$. Given an Automaton a function with the given pitype should Select a word accepted by it.

As far as I understand, in a basic dependently typed lambda calculus, both types suffer from the same problem: Their elements can never be introduced. Neither is it possible to select an element from the type $\bot$ nor select a word accepted by an automaton that doesn't accept any words.

I was wondering, if partial functions may be a solution to that problem. But how are partial functions are represented in a typed lambda calculus? An easy way I can imagine would be to be to create expressions, that allow the introduction of partial functions, such that there simply are no computation rules for undefined inputs.

So my questions are:

• Does that make any sence, and is it common to solve this kind of problem that way? Is there good literature?
• If the approach seems legit, is it possible to distinguish partial function types $A \rightharpoonup B$ from regular ones $A \to B$?

Note on the purpose: To be honest, I haven't formalized automata in any calculus, since for now I mostly would like to steal the concept and notation of dependent types and use them in my work to get across a concept. But if what i will do isn't completely bogus, it would maybe at least leave open a possibility to formalize things later.

A choice function of type $\prod_{D:\mathcal{U}} D$ is meant to represent user input - which should be non deterministic .. so there would also be no congruence)

• Bonus question: Can non-deterministic functions be represented in a calculus such that this may be expressed?

Answer 1

It is possible to take a typed lambda calculus and add general recursion or fixed points. See for instance Plotkin's PCF, or HOFL in Winskel's formal semantics book.

In that way, one keeps the type system but introduces partiality. This is a very common approach for Turing complete typed programming languages.

Of course, now the logic associated to the calculus via Curry-Howard is no longer consistent, since every type is inhabited (by non terminating terms). This is not a serious problem for programming.

If wanted, in the type system one could distinguish between terms involving general recursion (which might not terminate), and terms involving no recursion or some known-to-be-terminating one, like (higher-order) primitive recursion. Note that this will not separate the programs between "halting" and "non-halting", which is undecidable, but only between "statically known to halt" and "statically unknown to halt -- they might or might not".

I have not thought much about that, but intuitively a non-termination monad would fit nicely in such type system. With a non-deterministic monad, one can also address non-deterministic functions.

A final comment: after reading the question, I am actually more concerned about the posted automaton-based example than termination. With dependent types, one can use the $\Pi$-type of a selection function (as the one which was posted), which given an automaton return one of the accepted strings (or a "empty-language" token). However, let's keep in mind that when a dependent type system checks a term against such $\Pi$-type, the term must contain the recipe to generate the string, as well as a proof that such string is accepted by the automaton. The posted question, in my view, seems to forget about that -- as if the type system could check any algorithm correct (in the sense of returning an accepted string). This is not possible.

Answer 2

There is nothing that prevents dependent types from declaring:

$$T: a \rightarrow a \rightarrow bool$$

If you can then prove, or if you assume:

$$\forall x,y,z(T(x,y) \wedge T(x,z)\Rightarrow y=z)$$

You then know that $T$ is a partial function. You can then use a maybe type and define:

$$T(x,y) \Rightarrow t(x) = \mathbb{just}(y)$$

$$\neg \exists y T(x,y) \Rightarrow t(x) = \mathbb{nothing}$$

Which gives you a function of signature:

$$t:a \rightarrow \mathbb{maybe}\,a$$