winterkoninkje: shadowcrane (clean) (Default)

I was thinking recently about the design of a language which makes pointedness explicit in the type theory. That is, there are benefits to working in provably-total languages, especially when it comes to the equivalence theorems you can prove; however, there are also benefits to working in non-total languages (namely, not needing to prove totality). Previous approaches to this sort of thing have been based in domain theory; in particular, they've been based on pointed cpos (cppos)— i.e., a cpo with a least element, representing the total lack of information, which is often conflated with nontermination. But there's a problem with this.

The problem is, there are some cpos which have a least element (and hence are technically cppo) but where that least element cannot or should not be conflated with nontermination. In particular, product domains are formed by the tupling of elements from various domains. Thus, given A = \Pi_{i \in I} B_i, if all the B_i are cppo then it follows that A is cppo: the least element of A is the tuple taking the least element of each of the B_i domains. However, the least element of A is not nontermination— it's a tuple (whose components may be nonterminating). That is, we can perform eta expansion of A, without running into the various issues that arise for Haskell's tuples. In the limit we can consider the product of the empty family of domains (aka, the domain with a single uninformative value), and this should not be confused with the result of lifting the empty domain (aka, the domain with a single non-terminating "value").

So clearly, if we are to use domain theory to reason about termination, we must distinguish cppos which are pointed by nontermination, vs cppos whose least element is eta-expandable. However, I'm not sure that this distinction has been made before in the literature...

winterkoninkje: shadowcrane (clean) (Default)

In formal treatments of lazy functional languages like Haskell, appeal is often made to domain theory. For those who aren't familiar, a domain is nothing more than a set equipped with an ordering relation that obeys certain laws. The ordering relation captures a notion of "informativeness" whereby "greater" elements are more defined or more known-about than "lesser" elements. One of the particular laws is that the domain must have an element, ⊥, which is less than all others (and therefore contains no information other than what domain you're in).

Another way to think about domain theory is from the context of logic programming. The domains we often encounter in functional programming are defined structurally. That is, given an algebraic data type, we can construct a domain for the type where the elements of the domain are generated by its initial algebra on a set of variables representing unknown substructure. Indeed, this is usually the domain we are most interested in. In this case, ⊥ is simply a free variable (and thus, is actually ⊤). If we treat the variables as logic variables, then the domain ordering is defined by the subsumption relation induced by unification (aka pattern matching). Thus, a domain is simply the set of all patterns we could write for some type, and the subsumption relation between those patterns.

In Haskell we often conflate "⊥" as a domain element we know nothing about, and "⊥" as a non-terminating computation. There are natural reasons for doing so, but it's unfortunate because it loses a critical distinction between what is already-known and what is knowable. This raises questions about how much of our domain-theoretic training we can carry over to total lazy languages, a topic I've become quite interested in lately.

The idea that non-termination and free variables are the same comes from the idea that if we try to case match on an unbound variable then we will deadlock, waiting for that variable to become bound to something in order to proceed. In a fully interpreted language this holds up fairly well. However, in languages which aren't fully interpreted (e.g. dependently typed languages, languages with non-ground terms, parallel data-flow languages) it doesn't hold up because variables serve multiple roles. Depending on the context, we will want to think of a variable as either being bound to no element of the domain, or as being bound nondeterministically to every element of the domain. The former matches our functional programming intuitions about non-termination, whereas the latter matches our logic programming intuitions about non-ground terms presenting the type of all the terms they subsume.

In particular, the idea of variables bound to everything allows us to consider the idea of a hypothetical input: an input about which we know nothing, but which we are permitted to inspect for more information. Case analysis on hypothetical variables is the same as reasoning by cases in proof theory. These are different from abstract variables, which are values about which we know nothing and which we are not permitted to inspect. Loosely speaking, hypothetical variables are those introduced by universal quantification, whereas abstract variables are those introduced by existential quantification. (However, existentially bound variables may still by hypothetically analyzable rather than being held abstract; it depends on the situation.)

In a total language we are not permitted to write computations that we cannot prove will terminate. Thus, we can never obtain a nonterminating 'value' inhabiting the bottom element of a domain. However, we can still use bottom to represent things we hold abstract or which we don't force the evaluation of. Thus, in a total lazy language, domain theory should still have a role in strictness analysis and certain other formal reasoning. Given a domain we can interpret it hypothetically, as we do when performing strictness analysis or reasoning by cases, or we can interpret it abstractly, as we do when performing termination analysis. This conflict feels very similar to the conflict between parametricity and dependency. I wonder if any work has been done on this domain theoretic duality?

RSS Atom

April 2019

S M T W T F S
 123456
78910111213
14151617181920
212223242526 27
282930    

Tags

Page generated 7 Jul 2025 04:35 pm
Powered by Dreamwidth Studios