Lambda the Ultimate

I am working on the design of a language (Albatross) which allows for static verification. It has a strong functional core. One of the most important types in a functional language is the inductive or algebraic type. One of the most prominent examples is a list. E.g. a list type in Albatross is declared as follows.

A: ANY
class
    LIST[A]
create
    []
    (^) (head:A, tail:LIST[A])
end

It has the constructor [] to create an empty list and the constructor ^ to construct a new list by prefixing an already constructed list (tail) with a new element (head).

From a nonempty list we can extract the head and the tail with the following functions.

head(l:LIST[A]): A
    require
         l as _ ^ _
    ensure
        -> inspect
               l
           case h ^ _ then
               h
    end

tail(l:LIST[A]): LIST[A]
    require
         l as _ ^ _
    ensure
        -> inspect
               l
           case _ ^ t then
               t
    end

The functions head and tail reverse the effect of the constructor ^. I am looking for a name on how to describe these type of functions.

The most immediate ideas are _desctructors_ or _unconstructors_ which I don't find very appealing. A better name might be _inverse constructors_ which seem to precisely describe what they are, but sound a little bit clumsy.

Does anyone have a good idea on how to name these animals?

Some background information on why I need these type of functions:

Algebraic data types are a great tool, but they are not always the appropriate tool. E.g. in order to describe natural numbers their implementation is straighforward but awfully inefficient (this is one of the big problems when you want to extract source code from Coq). There are two ways to describe natural numbers with an efficient implementation. Either as machine numbers with modulo arithmetic or as arbitrary sized numbers where the components are machine numbers.

Machine numbers are not objects of algebraic type. But they are similar. The have constructors (zero and successor) and an induction law. Furthermore they have discriminator functions (n = 0) to decide how the number has been constructed and an inverse constructor (predecessor).

As soon as a type has an induction law (which implicitely defines the constructor functions), discriminator functions and inverse constructors the compiler can treat these types like inductive types in order to define recursive functions (which are guaranteed to terminate), do pattern matching etc. The discriminator functions and inverse constructors are necessary for the compiler in order to be able to compile pattern matching expressions into executable code.

In my opinion these pseudo algebraic/inductive types will be a great tool. Therefore I need good notions and names to express properties well.

Thanks for any help.

Language Description