How to name the inverse functions of constructors

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

'Deconstructor' has always

'Deconstructor' has always seemed like the obvious name to me, though I haven't actually seen it used for the purpose.

It makes sense from an English language point of view, and avoids the confusion of using the word 'destructor', which already has a different meaning in many programming languages.

By Michiel Helvensteijn at Mon, 2016-11-07 11:47 | login or register to post comments

Seconded

I’ve always liked construct/deconstruct as well. “Destructuring” (as in “destructuring assignment”) is pretty good, and more widely used.

“Destructor” is a red herring—it comes from “destroy”, not “deconstruct”. Plus, “destroyer” would be too bold.

By Jon Purdy at Wed, 2016-11-09 04:35 | login or register to post comments

unapply

unapply (at least in Scala).

By Sean McDirmid at Mon, 2016-11-07 21:40 | login or register to post comments

Extractor

http://docs.scala-lang.org/tutorials/tour/extractor-objects.html

The unapply method is how you define an extractor (hope this is still true...)

By Burak Emir at Sat, 2016-12-17 01:37 | login or register to post comments

short vs long

Do you want a short and punchy Anglo Saxon style, or a long and multi-syllabic Latin style? Both choices can cause ambiguity. Long names get vague via per-syllable sense tuning. Short ones are often already taken, and many folks hate overloaded words. It also sounds like you want nouns. I'll suggest verbs, and you can noun-ify them by appending "er" or something.

I have used make for constructor before, and ruin for destructor. (No one likes to pronounce ruin clearly, and it looks like run to some people.) For the inverse of make you can use unmake or ekam. The former is easy to pronounce, while the latter recalls word-reversal usage from an earlier generation. Brevity makes it easier to point out the difference between ruin and ekam. Lots of syllables can demand more cognitive processing.

By Rys McCusker at Tue, 2016-11-08 00:04 | login or register to post comments

make and break

cons is a maker

car and cdr are breakers

endp or null is the end-stop or just stopper

By Alan Crowe at Mon, 2016-11-14 20:58 | login or register to post comments

compose / decompose

compose / decompose
build / unbuild
assemble / disassemble
develop / undevelop
do / undo
unfold / fold
hi / bye :-)

By Ivan V. at Tue, 2016-11-08 09:49 | login or register to post comments

Distiller?

Kind of matches the physical process of separating a mixture to recover its essence.

A slightly more common term for the same might be a separator or an extractor.

By Andrew Moss at Tue, 2016-11-08 09:55 | login or register to post comments

Surely we're talking about

Surely we're talking about accessors here

I can't see car and cdr as somehow inverses of cons. cons creates a pair from two other things, but car and cdr merely give a direct reference to the encapsulated things; they don't destroy the pair, or remove the objects from the pair.

The opposite of cons, surely, has to be the underlying deallocation operation.

<edit> damn, replied to the wrong message.

By simon.stapleton at Wed, 2016-11-09 11:01 | login or register to post comments

Top-level reply?

I couldn't work out which message you were intending to reply to - top-level response to hbrandl?

Anyway, after rereading each of the posts you are correct that what is being described is not really the inverse operation. But it also seems that is not really what hbrandl is asking for on a reread.

The structure being described as being similar to ADTs, but different, is the structure of a group, rather than an algebra. I could not find an adjective that meant "being group-like", but given that the description is actually of operations that preserve the group-structure in the types perhaps Homomorphic Data-Types would be an appropriate name?

By Andrew Moss at Wed, 2016-11-09 13:57 | login or register to post comments

Record Accessor Functions

Interestingly 'head' and 'tail' have the type of record accessor functions.

So we can view the definition of 'cons' as a record with fields named 'head' and 'tail'.

By Keean Schupke at Tue, 2016-11-08 17:29 | login or register to post comments

inverse functions

Hbrandl, may I ask a thingie?

I'm not sure what is really the matter of the question. Are you having in mind some relation like functions and their inverse functions in math? Like when you have a single equation, you can express y in terms of x, or x in terms of y, all from the starting single equation?

I assume the same could apply universally to any function in programming (not just in math), even with multiple parameters, so we can automatically express each parameter in terms of other parameters, together with the result, regarding to the body of the function. If that is what you have in mind, I'm really interested in discussing this matter, as it would be a great extension to the current programming technology.

But again, maybe I dream too much...

By Ivan V. at Wed, 2016-11-09 17:43 | login or register to post comments

I am afraid I don't

I am afraid I don't understand your question. Would you please explain a little be more in detail what you mean?

By hbrandl at Thu, 2016-11-10 15:35 | login or register to post comments

details

Let's say, for example, that we have a function


function y (x: int): int

After defining some function body, we can calculate a value of y by providing the parameter x. Wouldn't then be nice if we could, in another attempt, provide a value of y and calculate a value of x from that? It would be like answering a question: what should be x to get a known result y? Now calculating y from knowing x, and calculating x from knowing y, is mutually related as a function and its inverse in math.

In math, we can transform expression y = x + 1 to x = y - 1 using algebra rules, depending on what we want to calculate. Somehow it seems to me that this could be extrapolated to any function in programming, not just in math, but I think that that algebra is not invented yet. I'm still not sure what impact on the programming technology would this have.

But maybe this problem is even unsolvable in terms of programming functions.

By Ivan V. at Thu, 2016-11-10 16:52 | login or register to post comments

Thanks for the details.In

Thanks for the details.

In Albatross you can define the inverse of a function provided that the function is injective i.e. invertible. See for example in the chapter Quick Tour in the section "Function Type" the function origin which maps y back to x.

However such a function in Albatross is a ghost function i.e. a function which can be used only in assertions because by just defining it there is not yet any algorithm given to compute it. In order to make the inverse of a function usable in computations you have to provide an algorithm.

By hbrandl at Thu, 2016-11-10 17:20 | login or register to post comments

Injective ⊊ Invertible

In Albatross you can define the inverse of a function provided that the function is injective i.e. invertible.

These terms are not the same, and you probably don't want to confuse them. (For example, the succ function on natural numbers is injective, but not invertible.)

By L Spice at Fri, 2016-11-18 19:24 | login or register to post comments

It depends on how you define

It depends on how you define "invertible". I usually characterize a function f as "invertible" if there exists an inverse g, whose domain is the range of the original function and whose range is the domain of the original function so that g(f(x)) = x for all x in the domain of f.

With this definition "successor" is invertible and any injective function is invertible. Its inverse is the predecessor function. However the predecessor function is not total. It is not defined for the argument zero. This corresponds to the fact that zero is not in the range of the successor function.

What definition of "invertible" do you have in mind?

By hbrandl at Sun, 2016-11-20 01:01 | login or register to post comments

Invertible = injective + surjective

What definition of "invertible" do you have in mind?

Towards the principle that a function is not just the 'rule', but the triple of the rule, the domain, and the codomain, the usual mathematical definition of invertibility of a (total) function from A to B is that it has a (total, two-sided) inverse from B to A.

Note both that there is already a perfectly good word for the concept you describe, namely the one you use, 'injective'; and also that, for a function that is not invertible in my sense, the two possible meanings of inverse (left or right) do not coincide. A function can have neither, or exactly one, but (unless it is invertible in the above sense) not both.

By L Spice at Mon, 2017-07-03 00:16 | login or register to post comments

Machine numbers

I do not think the OP is correct in saying machine numbers have constructors 0 and successor. Machine numbers are n-bit binary fields, with addition defined on that field. So for example an 8 bit machine number has 2^8 possible constructors, and a function 'add' defined as eight individual add with carry operations chained together. Add with carry is defined as a total function using logic truth tables.

By Keean Schupke at Thu, 2016-11-10 07:29 | login or register to post comments

Re: Machine Numbers

Dear Kean. You are right with respect to the implementation. Machine numbers are n-bit binary fields where n in one of {8,16,32,64}.

However I am trying to find a specification of these numbers which is semantically equivalent but which can be used to do verification. And I am trying to use as little axioms as possible. Currently I use the following axioms:

- 0 is a number

- each number has a successor

- each number can be reached by starting from 0 and applying the successor function repeatedly

- there is a greatest number whose successor is 0

- each number has a predecessor with n.successor.predecessor = n

I am pretty sure that I can derive modulo arithmetic (i.e. the usual arithmetic on 2's complement numbers implemented in todays CPUs) from these axioms. In addition I will probably need some axiom specifying that the greatest number is 2^n - 1 for some n.

In that view I can treat 0 and successor as constructors because all machine numbers can be constructed by them, I can derive an inducion law and therefore allow induction proofs and recursive functions with pattern matching.

Modulo addition can be defined as

(+) (a,b:MACHINE_NUMBER): MACHINE_NUMBER
    -> inspect
           b
       case 0 then
           a
       case m.successor then
           (a + m).successor

This function behaves like the usual addition function of the CPU. By compiling the code I can replace any call to the recursive function by a call to the corresponding CPU operation.

By hbrandl at Thu, 2016-11-10 15:55 | login or register to post comments

Verification

Verification of the CPU design can be done by SAT on the bit field. If add with carry is correct, chaining to n-bit is correct.

I am not sure what you are trying to prove? Are you trying to prove the CPU has a correct implementation of modulo arithmetic? As far as I know this has to be done exhaustively as there could be a single bit error at any stage if the CPU has production or design issues.

Given that proving the CPU arithmetic correct is a problem for the CPU manufacturer, you can just assume that machine integers are correct. In which case you can use machine integer words to construct 'infinite' integers, and you can just trust these are correct and use them in proofs, which is far more efficient than Peano numbers.

By Keean Schupke at Thu, 2016-11-10 16:04 | login or register to post comments

Sorry if I haven't expressed

Sorry if I haven't expressed myself very well.

No, I don't want to prove that the CPU implements modulo arithetic well. I assume that the CPU has a correct implementation.

I want to find a specification of the machine arithmetic which relies only on a couple of axioms and is easy to understand. If want to specify the user view of a machine number. The user view of a machine number is a natural number which is bounded and wraps around a the greatest representable number.

The number of axioms shall be very limited in order to be sure that the axioms are free of contradictions and specify exactly the behaviour of the implementation.

Based on the axioms I want to prove formally (i.e. verified by the compiler) all needed laws of arithmetic like commutativity and associativity of addition and multiplication, distributive laws ...

By hbrandl at Thu, 2016-11-10 17:06 | login or register to post comments

view (patterns)

A name from the functional programming community that may help you formulate the need is "view pattern": a view or view pattern is a function that takes a value and produces a "view" of it in a certain algebraic datatype that is meant for inspection. The internal representation of the data is in general distinct from the view(s) of it that are exposed for various reasons: encapsulation/state-hiding, correctness, convenience, performance, ease of reasoning (formal or informal...

By gasche at Thu, 2016-11-10 17:09 | login or register to post comments

This is really a great hint.

This is really a great hint. Thanks a lot.

I have googled a little bit and found a paper from Philip Wadler from 1987 which describes the concept very well.

He is addressing the same problem as I have: Use the clarity of inductive types (or free types as he calls it) and the efficiency of data abstraction.

It is always interesting to see that there is nearly nothing absolutely new under the sun. Phil Wadler's paper has been written 30 years ago!!!

By hbrandl at Thu, 2016-11-10 18:23 | login or register to post comments

Deconstructor was a common name at my college

Deconstructor is common in my part of the world, and I think still is a popular name in academic papers. In a compiler I worked on the abbreviation "split" was often used. I still use that name since it is short.

Of course you are free to define your own vernacular but I sincerely believe that deconstructor is that common it would be ill received.

(Btw. Never trust a category theorist. They'll try to tell you that theory can be defined in term of constructors, or deconstructors, solely. Which is idiot speak. They are dual, no constructors without deconstructors, and no deconstructors without constructors.)

By marco at Mon, 2016-11-21 08:49 | login or register to post comments

-

(double post)

By marco at Mon, 2016-11-21 08:49 | login or register to post comments

Inverses?

Theoreticians often use terms that "introduce" and "eliminate" things. I often speak of extractors as the things that get pieces out of things made by constructors.

However note, the thing which gets the value out of an inductive data type is not a function. Its a partial function: it only works if the value was put in there by the corresponding constructor.

At least my pattern matching system requires TWO entities: a checker with domain the constructed data type, which returns true if a particular constructor built it, and then a function with domain which is a subset of the type of the constructed data type corresponding to the values which can be created by the constructor, which returns the constructor's original argument. It is not safe to apply this thing unless the corresponding checker returns true.

So the "inverse" in my system consists of two "functions", not one. One could also define a function which returns an option type to combine these into a single function. However that begs the question, how to decode the option type. But then, a bool is also a sum type .. so that begs the question too :)

In language with pattern matching, the usual practice is to use the name of the constructor as the name of the deconstructor as well, and to distinguish them by context (if the name is in an expression, its the constructor, if its in a pattern, its the deconstructor). [I like to think of patterns as being "inside out" versions of the constructors]

So actually for a list, the correct external name is probably "Uncons". As Keeane pointed out, head and tails are the projections of the result of Uncons: they can't be applied to a list. Uncons of course, can't be applied to Empty (the empty list), so you would need "Unempty" for that. Which is basically a query if the list is empty or not.

Finally, you have to cojoin Unempty and Uncons, meaning, you have to apply both simultaneously to any list. Only one of them will work. This is what pattern matching does of course.

Head and Tail functions apply to streams, not lists.

By skaller at Tue, 2016-11-22 05:40 | login or register to post comments

Lambda the Ultimate

User login

Navigation