Lambda the Ultimate

At present pointer type &T is typed version of a linear machine address.

Now, one of the problems we have is that there is an unbounded set of mutations on the store a pointer points at, so it seems impossible to abstract them without performance loss. For example increment the value pointed at is an atomic read/modify/write operation that can't be broken down into a get/set sequence.

Furthermore C bindings can be polymorphic on pointers for example:

fun incr[T] : &T = "++*$1";

(where $1 is the argument) and this won't work unless we can distinguish C compatible pointers and the extended type needed to address a compact linear type.

The problem here is that pointers have two operations, get and ref and ref is a lot more general that mere set.

Now, I could do the incr thing by adding the following overload:

fun incr[T:COMPACTLINEAR]: &T = " ....";

if only there were some way to say that a type is compact linear (as indicated).

But then we're looking at either subtyping and classes of types of meta-typing or kinding, and that's a major system upgrade I don't know how to do right. The compiler *does* know when a type is compact linear, and Felix instantiates away all type variables so at least the back end knows.

Surely pointed at memory can be abstracted to three operations, 'read', 'write' and 'mutate'. Read and write can use 'get' and 'set'. For 'mutate' you need reference types. Given a type 'Ref A' any operation on the value actually happens at the address pointed to, so:

f (Ref x) = ++x

Would increment the value pointed to, not the pointer. What we want to do is separate dereferencing from the structure.

Edit: Therefore a mutable array would need to provide addressing and dereferencing, so if "p" is the base pointer and "x" is the index in the array, then the final address is "p + x". This then needs to be dereferenced, 'C' uses '*', but I will use 'deref':

++deref(p + x)

would increment the value at the address pointed to by "p + x". The point is all addresses are just plain integers of the appropriate size (we consider them as offsets from zero, but like C/C++ we can encode the type of the thing pointed to in the pointer type so ensure we can only point to the start of multi-word structs). We cannot express the type of 'deref' in 'C', but we can in C++:

template <typename T> &T deref(*T)

I don't see how this helps apart from the fact the whole idea was to get RID of references :) In fact you cannot express it in C++, because &T is not a type, no matter what the C++ Standard says.

You should just think "bitfield". If you want to mutate a bitfield of 3 bits the type is 8 so we have this pointer type in Felix:

&8

but this is not enough information, because we do not know WHERE in the machine word those 3 bits are.

So actually we need a pointer to the machine word and 3 extra machine words to determine the location for an arbitrary compact linear type. The formula is

v = (w - d) / s % m

where w is the word, d is an offset which is required for sums, s is the generalised right shift amount obtains by division, and m is the generalised mask, obtained by modular remainder. For example if the type of a value is

2 * 8 * 5 + 52

then

v = (w - 52) / 5 % 8

is the value of the three bits.

So unless I generalise the representation of pointers, my type system is unsound.
Since compact linear types are statically typed, it is enough to use two pointers, one to the word containing the component, and one to the triple of words d,s,m.

If I do that C compatibility is out the window. So I have to find a way to use the generalised pointers when required and optimise the second machine word away when not required. C of course doesn't have general compact linear types, but it DOES have bitfields.

There are two difficulties with Proxy: the first is that it requires a fixed set of operations. The second is probably more serious: how does this generalise to support pointer projections? Remember a record has named fields so we just overload the field name with argument types T and &T. A compact linear product has projections too, but how do we overload them for an abstract type?

Remember the whole point of structural typing, and types like 3 * 4, is that the type dictates the operations based on its structure. I have no idea how to preserve the structural information with an abstract type. If there's an abstraction here it's something like "product formation".

A compact linear type is a generalisation of "bit fields". For products, consider a type like 3 * 4 * 5, this means the first component has 2 values, the second 4, and the third 5. These are sums of units, eg 3 = 1 + 1 + 1 where 1 is the type unit with value ().

A good example perhaps is a clock: 60 * 60 * 24. The time in seconds, minutes and hours (only sums don't automatically have addition).

The most well known unit sum is 2, which is also called bool. Most language use nominal types for sums, but Felix also has anonymous structurally typed sums, and special notation for sums of units.

Compact means the values are bijection on a subrange of integer 0 .. n-1, and linear just means integer.

The point is by coercing a compact linear type to an integer you can add 1 to it, and then convert back, and thereby iterate over all possible values. In particular if you have an array with index type, say, 3 * 4 * 5, so it is rank 3, you can fold over all the elements without needing to know the rank.

There are other obvious uses. For example plain old 2^30 gives you a 30 bit unsigned integer this way, which is also a bit array of 30 bits. Although expensive to access the components, in some applications (eg networking) data compression is more important than decoding time.

So, compact linear type stores "2 * 4 + 6" type value as an integer value between 0 and 14? If I got it right, we want to be able to:

1. convert component values to internal CLT format; and
2. convert internal CLT format back to component values

Ok, that makes sense, but I don't see this as bijection. For example, an internal value, being of TYPE "2 * 4 + 6", could be "8", but the same "8" can stand for two different COMPONENT COMBINATIONS:

1. "2 * 2 + 4"; or
2. "1 * 4 + 4"

which makes the whole system as not bijective. If this theory holds, the internal format for storing CLT shouldn't be just plain bounded value range, it should also carry some other informations to make the system bijective. But then, are we loosing an essence property of fast itterating over all possible CLT combinations?

.. an algebra (as you proposed above) to injectively connect component combinations to internal values, I guess you did the math behind...

I can see the purpose of having a product of values, but what would be the purpose of having a sum of values or exponential values?

Well the original motivation is for array indices, which is why 64 bit limitation is reasonable. So a typical thing is like this:

var x : (double ^ 5) ^ 3;

This is an array, length 3, of arrays, length 5, of doubles. A double would be found by the formula

x . i . j

where i:3 and j:5. But now consider this isomorphic type:

var y: double ^ (3 * 5);

which is accessed by

y . (i,j)

and I get confused remembering the ordering. The index is called a multi-index and this data type is called a matrix. A matrix is NOT an array of arrays but it is isomorphic to one. And now consider

var z : double ^ 15;

which is an ordinary linear array. That one has only a *single* index so a fold over a linear array of doubles will also fold over a matrix the same size if you coerce the type first.

So what would this mean:

var a : double ^ (2 + 4)l;

Well it means you have two arrays, one length 2 and one length 4, next to each other making a total length of 6. The last value looks like

a. ( case 1 of (2+4) (case 3 of 4)

which is pretty messy looking. (In Felix the case index is 0 origin).

Now, that the compact linear type system seems sound to me, may I propose the following (I was holding this before the check):

You know how to hold a compact linear type inside a regular type, but how about other way around? Isn't a regular type value just a form of CLT where the length of CLT is just one element? If you could manage to hold regular types inside this one element CLT, you could have any type wrapped inside CLT type. So, for complex CLT-s, you would have regular type values wrapped inside CLT, and those regular types could again can hold another CLT-s. I think this tweak deals with interal byte representation of CLT-s and I don't know what impact to performance it would have, but it looks like a fractal to me and I like fractals :)

A further thought after realizing what sums, products and exponentials are is: maybe you could express any type as plain CLT and have just a single kind of treatment for pointers, element extractions and other operations?

You seem to be confusing sum and product types. With (2*4)+6, we have either a value from type (2*4) on the left OR a value from type 6 on the right, not components of both. But within the type (2*4) we'd have a component for the 2 and a component for the 4 (thus three bits). Or translating to a common language:

type (a + b) = Left a | Right b
type (a * b) = Pair a b

There are multiple possible encodings. But the range 0-13 can encode all the possible values of (2*4)+6. So if it's 0-7 for the (2*4) and 8-13 for the (6), the value 8 would mean the first choice of 6.

Obviously the encoding will be dependent on the type structure, since that (6) could be a (2*3) or a (1+2+3) or a ((2*1)*(0+(3+0))) or similar.

Edit: from your subsequent comment

what would be the purpose of having a sum of values or exponential values?

A sum of types (not values) is choice/conditional. The trivial example is booleans (`(1+1)` or `False | True` or `Left () | Right ()`), or optional values (`(1+a)` or `None | Some a` or `Left () | Right a`).

Exponentials correspond to functions, an arbitrary translation from a→b can be encoded as a number less than b^a. For example (Bool*Bool)→Bool (aka (2*2)→2) covers every possible binary boolean function - there are only 16 of them.

thanks for the simple explanation.

Here is something to think about: I cannot help not to connect CLT solution to a parsing technique that just came to my mind. We can use products for sequences and sums for alternations, and pack them in CLT format. Now, if we can iterate through all the combinations, just by simply incrementing a CLT internal value, then by extracting components in each iteration we could get all possible parse searches, which would be used to construct a parse forest.

Yes, a CLT is a limited kind of regexp (without recursion but with finite iteration due to exponentials).

But then, a type is nothing more than a grammar. Alternatives are sums, sequences are products. And recursion is recursion :)

Alternatively, a grammar is nothing more than a type.

And what do types do? Well they define a set of possible paths you can use to explore some data.

Everything in CS and maths is related. Sometimes the relations are hard to see or express so mathematicians invented Category Theory to makes sure NO ONE could understand it.

I like seeing grammars as fractals of all possible programs that some language can hold. Wow... How many combinations... It would be interesting to define a program, and then somehow to automatically find its equivalent that is optimized either for speed, either for memory usage. I've heard of "Simplex method" somewhere, but I never made myself to examine it. And there is also some funny called method from math theory, "jumping from rock to rock" in a rough translation from Croatian, dealing with the shortest path between two rocks. "Monte Carlo" method name also comes to my mind, I don't know why...

I think it shouldn't be so complicated, all we have to do is to state equivalences between sets of code fragments in some language, input an unoptimized code, construct a code fractal, and then run a statistical analysis, waiting for the result.

Anyway, I think that we can expect an exciting future with designing programs. Imagine getting a program that is proven that it can't get any faster... or smaller... Wow again...

[Edit] I just hope that halting problem undecidability is not in our way.

In general, it is :-)

What you are describing really IS done by low level optimisers. You look at several possible sequences of machine instructions which do the same thing, and calculate which is faster (no one gives a hoot about size any more only speed, but it turns out that smaller is faster on modern processors because of caching).

Unfortunately, static analysis is almost impossible because no one is going to say how many clocks an instruction takes! It's so variable, because the hardware people do their own optimisation, defeating compiler optimisations.

Some code, such as the Atlas math kernel, solve this by actually running competing examples and building the library with the winner. It takes over 24 hours to install Atlas on a medium speed machine.

I think that you would find this paper by Henry Massalin quite interesting. There is a GNU implementation of the technique somewhere, although it does not scale very well.

Interesting how some of optimizations are not even close to what would one expect (as a combination of instructions). Avoiding jumps sometimes seems inconceivable by a human thought.

I know what a sum type is :-) At least, in the usual functional programming sense. Your calculation is the same as mine.

In Felix the exponential written A^B is an array. For example:

var x : int ^ 3;

is an array of 3 integers. The 3 there is a type, the type of the array index. It a synonym for 1 + 1 + 1 = unit + unit + unit. This variable:

var y = int * int * int;

is the exact same type. This is a design decision, that the isomorphism should be an identity. It means that arrays are just a special case of tuples. The type written

3 -> int

is a function. So both arrays and functions are exponentials, they're both mappings***. The difference is arrays also support mutation, functions do not:

&x . 0 <- 42;

assigns 42 to the first component of the array x.
As a value, however, the array is purely functional.

The interesting thing about Felix arrays is that the index can be ANY compact linear type. As it happens if the index is a sum type this corresponds to array concatenation.

The key point about compact linear types being compact and linear and small enough to fit into a machine word is that you can then fold or map over the array with a single linear operation, independently of the index type. All you need to do is coerce the index type and the fold or map (or whatever) adapts.

*** its annoying that a function f applied to a value v is written f v. However an array a indexed by i is written i a. In fact, this is a shorthand, the real operation is an application of a projection number i to the array a. So the array is an exponential but it is not applied to the index, the index is applied to it. I wish I could see a clean way around this conflict.

I'm not sure if part of this is a good idea, though. Isn't it dangerous to think of a*b and b*a as identical types? Seems like you're missing a chance to report a likely error.

 So the array is an exponential but it is not applied to the index, the index is applied to it.

Hmm, but does (a i) work as long as you're only interested in treating a as a function? My thinking is along the same lines as yours in many respects. Felix seems interesting. I wish it were pure :).

a*b and b*a aren't identical.

You can do a coercion chain:

(3 * 4) :>> 12 :>> (4 * 3)

So you're explicitly applying two isomorphisms. If you're doing this to a matrix index then you're changing the scanning order if you're using a pair of loops. This is physically safe.

It's not clear if it makes sense. One could even weaken the rule. For example why not allow

12 :>> 10

I mean that just chops the end off. Quants often get slices of matrices.

So the net result is that reshaping coercions are more powerful than one might like, they can do a bit more than you can do with Jay's method which only allows applying associators to data functors.

As to purity: as in Ocaml, you can write pure code. What's more, you can write pure functions which use dirty impure internals which do not escape. Even more important, using coroutines there is a strong notion of purity even for imperative code. For example:

chip series 
  connector io
    pin inp: %<int
    pin out: %>int
{
   var sum = 0;
 again:>
  var x = read io.inp;
   sum += x;
   write (io,out, sum);
   goto again;
}

This is imperative code but it is obviously pure. It has no side effects. And it does something you cannot do natively in a functional programming language. It handles streams.

In general functional systems can't handle coinductive types. Cofunctional systems can. Of course in an FPL you can *model* a sum type, and you can *model* a partial function and you can *model* a stream and you can even *model* state mutation. I mean, Turing complete means you can build an interpreter that can do anything computable. But coroutines handle these things natively. Functional code is purely spatial, that is, declarative. Cofunctional code is temporal. Programming without a space/time continuum is absurd :-) Literally, action is the space/time conversion, you really need both.

So functions are not enough. Yes, we want purity and Felix allows it but does not enforce it because I don't know enough to do that.

My take on purity is that what's important isn't building things out of functions, but rather the ability to view mutation as a series of values in time. You're right that having this view and typing it soundly are somewhat orthogonal.

What's a good resource for learning about Felix? The website seems spartan.

Well .. try some links, there's a reference manual and a couple of tutorials online.
And a reference manual (PDF) here

https://github.com/felix-lang/felix/blob/master/felix-ref.pdf

which at 300+ pages isn't quite spartan.

Jan 20 already - are you in NZ? (Edit: Nevermind, your bio says Australia.)

Sydney Harbour to be precise :)

Yes, we can convert from a compact linear type to a subrange of integers and back. In fact in Felix, the idea is that conversion, in both directions is a pure type cast, that is, the bitwise representation is unchanged so the performance cost of the conversion is zero.

The encoding is fixed in the compiler. I admit I forget the ordering. The "other information" required given the compiler's fixed algorithm is just the type.

For products, the formula is well known, it is nothing more than an ordinary positional number system for natural numbers. For example the time

hours, minutes, seconds

is just ((hours * 60) + minutes) * 60 + seconds = hours * 3600 + minutes * 60 + seconds * 1.

So the time of day is from 0 to 86399 seconds, for a 24 hour clock. This is obviously a bijection. I forget if you write this hours, minutes, seconds or second, minutes, hours in Felix :)

the type is written

24 * 60 * 60

assuming bigendian ordering (I forget, i might have used little endian).

Well this project started over 20 years ago, and the critical requirement was to support large numbers of lightweight threads (of the order 100K). The environment was telephony (so one thread per active phone call).

Today, it is still the only language I know of that can do this, apart from Go, and Go is crap (I mean, no parametric polymorphism? Are you kidding?)

So to answer your question: at present pointer types do indeed require addressable store. The addresses will usually be on the heap. The GC is a naive mark/sweep not a copying collector so there is no moving things about. It has to be because the language is designed to bind to C/C++ and it would be too hard if the GC moved a pointer that C/C++ had borrowed.

And hence the problem: bitfields or more generally compact linear type components are not addressable by a single machine address.

Yes, I looked at Bananas/Lens etc, there's some support for some of it.

The "purely value based" comment is meant to mean there are no "lvalues" (C) or "reference types". References are not types. C lvalues are syntax rules that don't generalise.

A type system is a logic that models permitted semantics. Different logics model different semantics. If the logic models the permitted semantics of references correctly, then that logic can be used as a sound type system for references. To say references are not types is true, but you can model the semantics of references using types, which is all types ever do anyway.

Type system has to be combinatorial or they're not type *systems*. In particular care has to be taken with polymorphism.

If T is a type, so is T*, a pointer to T. But T& isn't a type because & is not combinatorial. In C++ this comes down to rubbish in templates if your T was say int& then T& becomes (int&)& which is nonsense. On the other hand int** is sane.

In C++ references could be allowed in function parameters, since there it changes the type of the function. That is, the "&" bit is part of the function type, it's not part of the argument type.

There is nothing wrong with "Ref(Ref Int)" it would still look like an Int lvalue. Yes C++ does not get this right, but that does not mean the concept is flawed, just the implementation in C++.

Templates are not a great way to achieve generics either, so I would not use them as an example. Parametric polymorphism is a better starting point in my opinion.

Edit, I agree that pass by reference is part of the function type, but this has the problem that we don't distinguish between mutable locations and values in the type system if we do this. We cannot tell if a variable is a valid lvalue from its type.

It is not being able to tell if a term is an lvalue from its type that results in needing a syntax rules. To do this properly without syntax rules requires being able to determine from the type of any free term whether it is an lvalue.

There is nothing wrong with Ref(Ref Int) if Ref is a combinator. As it is in Ocaml. And as Pointer is in C, C++, and Felix.

However it is not a reference in the C++ sense of an lvalue in that case.

In C, lvalue is a syntax rule. In C++, lvalue is a type rule. Its a supreme mess! The C++ rules are not combinatorial and they also happen to be unsound. I tried to stop this crap but failed: C++ has a type thing called a decl_type separately from an expression type (which is separate from a value type!!)

Decl-types are used to do template meta-programming because the type system is totally broken, and you just can't handle all the cases without them. But the result is absurd.

My point is that pointers are first class values, and the pointer symbol in a type is a combinator, which captures the fact that they point at mutable store.

Felix does not require any type rules, nor does it require any syntax rules. More precisely if you have a "var" variable named "x" then "&x" is the name of the pointer to that store. You cannot use "&" in front of an expression or variable of "val" kind. Really a variable IS a pointer, but instead of having to deference it when you want the value stored there, Felix does that automagically and the "&" symbol suppresses the dereference.

If you insist, this is a syntax rule, but there's exactly one trivial rule. You can also get pointers to objects on the heap. The point is to address *components* of a product without any notion of lvalues or reference, one has to do address calculations on the pointer to the whole product to find and add the offset of the component.

Which Felix does using the *same* notation as used to fetch a component value, only applied to a pointer to the product type instead of the product type.

var x = 1,2;
var x2 = x.1;              // x2 == 2
var px2 = &x . 1;       // points to second component of x
px2 <- 42; // x == (1,42) now

This machinery is the same as used by C for arrays, however C cannot do this for structs, you have to use offsetof macro. C++ has pointers to members which can do this in a well typed way, however you cannot add pointers to members.

Since Felix uses projection functions, adding offsets is done by functional composition. This is what I mean by saying it's purely functional. All the address calculations are purely functional. Of course when you do a mutation using a pointer its obviously imperative code.

I should explain: there is no problem with variables having addresses.

The problem is that a variable might contain a value of a tuple type such as 3 * 4 * 5 which is a single machine word because its a compact linear type.

Now projections for values:

var x = (1, "Hello"); // type int * string
var i = x.0; // projection 0
var s = x.1; // projection 1

and the same notation for pointers:

var pi = &x . 0; // pointer to int type &int
pi

See? The projection is a PAIR of functions, one applies to a value of some type and one to a pointer. This lets us modify a component of a tuple stored in a variable by calculating the component's address from the variables address.

So now consider:

var clt = (true, false);

True and false are type bool which is 2, so clt is type 2 * 2 which is compact linear and so clt is a 64 bit integer with the low two bits holding the value.

But the bits aren't addressable. So whilst the value projections are OK, the pointer projections don't currently exist.

This is no problem with concrete types. The problem comes with polymorphism.
We don't know if

T * U

is compact linear or not. We can't disallow addressing the components if its not and we can't allow it if they are.

Which means the type system is unsound. (Or incomplete).

My point about (not) needing to invent a whole new language is that usually some other language is already coping with the requirement. (I won't say "solving the problem", because very often "the probelm" is asking the wrong question.) So:

And hence the problem: bitfields or more generally compact linear type components are not addressable by a single machine address.

... the bits aren't addressable.

Have you looked at BCPL's SELECTOR and BYTE constructors (and corresponding operators)? Here http://rabbit.eng.miami.edu/info/bcpl_reference_manual.pdf sections 2.14 and 4.6 for assignment thereto.

Beware that although BCPL is regarded as a precursor to C, it is considerably more 'close to the metal'. (I'm thinking that's a Good Thing in the case you're asking about.)

In particular, BCPL is completely untyped: all rvalues are whole words. It is up to the operator/function as to how that value is treated: INT or CHAR or STRING -- which is a pointer to a VEC. A VEC might contain CHARs one-per-word, or pack them several to a word; that's not type-checked: it's up to the program to treat the VEC consistently.

Pointers are again just whole-word rvalues. So BCPL needs distinct operators to apply a SELECTOR vs a BYTE vs mere dereferencing (monadic !) vs offset dereference (dyadic ! -- for example to index VECs).

Note in that manual section 4.5 'LEFT HAND SIDE FUNCTION APPLICATION', any function can appear on LHS of assignment. For the function/procedure definition, there's a library routine LHS() the function can call to determine whether it's selecting or updating -- the result for LHS() is planted by the compiler.