Lambda the Ultimate

Hi,

It's a call for kind help; in the form of more relevant pointers I seemingly have missed so far.

I am looking for authoritative reference materials about what people sometimes people refer to as "precise types" (in the programming languages ontology, preferably).

As most people on these forums I suppose, I believe I have grasped a fair enough notion of what we usually mean by static typing (as opposed to the dynamic side of things). The understanding situation on my end is way less comfortable re: "precise types".

I did try to read quite a bit of resources on typing systems and the corresponding, traditionally associated calculi schemes, and their respective, supporting nomenclatures, and I did stumble a couple times upon various phrasings of what the author is alluding to by his/her "precise types", but without really seeing a blindingly obvious common agreement and shared understanding of what is really meant, unambiguously, in a standard fashion by that : "precise types". It still seems to vary significantly from one author to the other.

For one thing, would that be an absolute notion for the qualifying criteria (like, e.g., when opposing a terminating vs. a non-terminating program, or inhabited vs. non-inhabited types, or confluent vs. non-confluent term rewriting systems, etc) or would that be something relative, with type systems offering features to denote "more or less" precise types ?

For another parallel, the signification of the difference (and implications) between the untyped lambda calculus and the many typed lambda calculi flavors one can devise are well understood today. I was expecting the case to be the same when one speaks of (more or less) strongly type systems, offering static type check convenience features but NOT qualifying as being frameworks for precise types, as opposed to the ones which do so. Therefore : if precise types are well understood today, which are the properties that the meta language / logical framework is supposed to have for one to be able to check about the precise types' inhabitation, its helper algorithms, etc, within the type system being defined or scrutinized ?

Thus, does someone know if "precise types" has been given a clearly delimited (small) set of definitions in the process of converging together, or is it still mostly left open to one's context of work (be it on type inference and/or just type checking, or etc) ?

If my question happens to be too much open for today's state of knowledge, I can provide what I (would like to) understand by the usage of the "precise type" phrase, say, in the specific context of static type inference during some compilation/translation process.

Thank you in advance for any relevant pointers.

Say we have the expression -

In my purely functional programming language (with strict evaluation), I currently handle the evaluation by returning a 'violation' value that describes the problem like so -

This ‘preserves’ referential transparency for all expressions by making all them replaceable by their value, if only by a violation. But this different than other purely functional languages I've seen.

Whenever I read a description of the properties of impure functional languages (such as ML), exceptions are described under the imperative section as an imperative feature. I find this a little odd as I'm not sure how a purely functional language would handle a division by zero error without exceptions (or without violations like I use).

Haskell has exceptions, but they can only be handled in the IO context. This makes sense to me because Haskell is lazy. My language is strict, so I don't see why I would be violating purity by having exceptions. After all, what makes a language purely functional is the pervasiveness of referential transparency (replacement of any expression with its resulting value). But why would we care about preserving referential transparency for the set of expressions that have no possible value in the first place? Would the replacement of violations in my language with exceptions technically render it 'impure'?

'FeML: a skeleton of a femto-ML with nothing but polymorphic variants and functions'
message at http://lists.canonical.org/pipermail/kragen-tol/2012-June/000958.html

As I said on the HN post, this sounds great but better options on the metal sound good - at the moment it's C or Forth. I would love to know what forum members think?