syntax for uniqueness

[John Skaller2]

So I can see no easy way to fix this:

var x = rev somelist;
var y = x + x; // ERROR

Its an error because rev now returns a uniquely typed list which can’t be used twice.

This is easily fixed by:

var x = unbox (rev somelist);

but doing so depends on knowing rev returns a uniquely typed object
and it looks ugly.


This problem doesn’t arise so easily with functions because of two factors:

1. Overloading

fun g (x: list [int] );
fun g (x: uniq (list[int]));
g (somelist);
g (rev somelist);

The appropriate g is selected.

2. Subtyping.

fun h(x: list[int]);
h (rev somelist);

This is fine because unique things are subtypes of their unboxed, non unique contents.

The problem with the variable case at the top of this email is that variables, having
names, are intrinsically sharable syntactically whereas expressions, being anonymous,
are intrinsically unique syntactically. In C, this is just lvalue vs rvalue.

In Felix, unique types stupidly apply to expressions or not depending on what the
programmers types them as. Variables screw this up. For example consider if
a variable JUST mean substitution EVERYTHING would be intrinsically unique.

For example

var y = (rev somelist) + (rev somelist);

would be the meaning of the original assignment, which is just fine.

In principle this is the meaning of “val” in Felix, so vals should always be safe
to use, and the compiler should share the store of a val in a var only when the
type is not unique.

All these problems stem from the notion of an object: a contiguous typed region
of store with a specific address which is itself a typed value called a pointer.
In pure FPLs use of pointers is generally implicit. For example typically the
C representation of a list by a pointer to a struct containing some value and
a pointer to another node (or NULL) is represented in an FPL by recursion
and the equi-typed interpretation of recursion, like:

typedef list = int * list + 1; // or
typedef list = int * alpha + 1 as alpha;

in Felix. The representation is the same as the C one but the user cannot “get at”
the pointer which occurs at the recursion point (list or alpha in the RHS of the above
definitions). One can say these lists are values, the object nodes are there in the
implementation but not in the language. Compared to the C like definition

struct listnode { x : int; next: &listnode; }
typedef list = &listnode;

The issue here isn’t mutability but the ability to alias the pointers which is
absent from the functional form. However BOTH forms are incapable of
allowing the mutation on uniqueness optimisation.

As a side note the slist type in C++ defined in the Felix repository
checks uniqueness dynamically by examining a ref count and is actually
much faster on average that even a compile time uniqueness condition.
Its not clear why one would not use ref counts for pure inductive types,
its really funny that constructive languages like Haskell want to use
a GC when constructing one value at a time out of other already existing
one cannot introduce a cycle!

It is in fact possible to create cycle if you have mutability (as in Ocaml
or most C like languages with explicit pointers and mutable store),
or if you use cheat constructions like “let rec” which make two objects
at the same time and allow the address of each to be used in the other.
In an FPL this typically cannot happen for data, but it does for
function closures, and that’s why a GC is required.

In conclusion there is a serious need for some proper theory to be
done which actually distinguishes values and objects from data structures.
The FPL style list is NOT a data structure, the C one is, and the difference
is in the accessibility of internal object addresses as pointers.

In other words I have no real idea how to solve the problem.
It occurred when as an experiment I changed just “rev” to state it had
a unique return type. It took a while to patch the Felix libraries and tools.
Map and filter should be patched too, but I think it would create a mess.
And that’s just lists. Its not clear the FPL style list shouldn’t be thrown
out and a binding to the C++ slist used since it can handle uniqueness
of PART of a list dynamically and so is not only more efficient, it needs
no type system support.


—
John Skaller
ska...@internode.on.net

[John Skaller2]

I’m still struggling with uniquness etc. So here are some thoughts.
Instead of trying to follow academia and Haskell I’m going to try a contract programming approach.

First, the values which are given unique (etc) types are references to some other resource.
The simplest example is a pointer to an object on the heap, for example a pointer to a C like
char array.

Four things can happen with C like char arrays.

1. Construction (using malloc and a cast).
2. Mutation, eg with strcpy of just a loop upcasing the chars.
3. Inspection, where the object is examined but not changed.
4. Destruction, eg by free.

Now, given a char pointer we can cast it to be unique. In Felix ucstr.pak,
class UniqueCStrings we have this:


open class UniqueCStrings
{ ...
// abstract representation
private type _ucstr = new +char;

// make it uniq
typedef ucstr = uniq _ucstr;

// privatise access to representation
private fun unpack (var p: ucstr) : +char => p.unbox._repr_;
private fun pack (p: +char) => p._make__ucstr.box;

// Constructors
ctor ucstr (var s:string) = {
var p = s._unsafe_cstr; // malloc'd copy of string contents
return pack p;
}

ctor ucstr (s:+char) => s.strdup.pack;
…


Given a Felix char array type

+char // C type char*

we can just cast it to be unique, as in the typedef above. But we could do this too:

var p = s._unsafe_cstr; // allocate by copying from a string
var up = box p; // make unique

This is dangerous because we have a copyable pointer p as well as a copy
of it in up which is specified as the only copy. Its not illegal, in fact this is what
the constructor ucstr above does. But what it does is safe, because on return
of the function, p is no longer accessible.

The point is that saying something is unique by using the uniq type constructor,
done by “box” on the value, is a promise by the programmer that this is the only
pointer to the underlying object. Importantly though, the promise does NOT have
to hold, as illustrated, it only has to hold at the first point where some other
operation might rely on the promise.

When is that? The answer is, to be conservative, just after the last point
where the promiser loses control. In ucstr, the promiser loses control
at the point of return (after pack is applied which boxes the sharable alias p).

What’s vitally important above is that pack and unpack are private, and _ucstr
is both private and abstract. This means outside the class, a value of type +char
can never be confused with a ucstr, even if it is boxed, and the ucstr representation
cannot be unboxed outside the class either.

So we are using classes and abstraction to ensure the uniqueness property of
our pointer can’t be messed with. In other words any error should be caught by
the type system OR be in the class definition.

So we do similar tricks to ensure we have a free procedure:

// deletes the store
proc delete (var p:ucstr) {
var q = unpack p;
free q;
}

The unique value p is unpacked, unsafely, to a sharable value q which
is used to delete the store. But when the procedure returns, p has been used
exactly once and the sharable q has been forgotten.

Now lets consider a mutation:

// modify one char
fun set (var s:ucstr, i:int, c:char) : ucstr = {
var cs = unpack s;
Carray::set (cs, i, c);
return cs.pack;
}

Here we unsafely unpack the unique value to a shared one so we can use
the set function to modify the char array, then repack it after the modification
and return that. This is a key point of uniqueness typing that such a routine
as set can be freely used to perform an update, precisely equivalent to modifying
a copy and returning that, that is, a functional update, preserving referential
transparency, but doing the operation more efficiently.

Internally the operations have effects, but the effects are localised to
the function and so they’re not side-effects. This is because no external
observer has an accessible copy of the parameter, because it is uniquely typed.

More definitely: the set routine *relies* on the honesty of the programmer
when uniquely typing the pointer, the class system and class abstraction are
used to help enforce that. Note again there’s no guarrantee the programmer didn’t
mess up, only that if they did mess up, they messed up inside the class.

Accessors are similar: (ouch, UCString doesn’tr actually have this but should):

// get one char
fun get (var s:ucstr, i:int) : char * ucstr = {
var cs = unpack s;
var ch = Carray::get (cs, i);
return ch, cs.pack;
}

However this an extreme pain to use!!

var p = ucstr (“Hello”);
def var ch, p = get (p, 1);

The problem is get has to return p, otherwise we have a memory leak.

==========

What do we want really? Its perfectly safe for a fuction to borrow a copy
of a unque pointer so as to access the underlying object, provided it doesn’t
modify it, and provided it *forgets* the pointer. Currently Felix uses a dangerous
hack to allow this: the uniqueness typing checking algorithm ignores address
taking. So you can take the address of a variable holding the unique pointer,
pass that to a function, which then dereferences it, unpacks the pointer,
and does the access. On return it just forgets the pointer. What the function
does is safe, but allowing uniquely typed variables to be addressed, and the resulting
pointer dereferenced clearly destroys the guarrantees. In other words, including this
feature makes the typing unsound. Its a hack because there’s no alternative if
the pointer is stored in a var: taking the address cannot be considered a use,
because the resulting pointer can just be dropped or copied.

The usual kind of rule in the literature is that a data structure containing unique
values must itself be unique (to prevent copying of the components, defeating
their individual uniqueness assurances). But this doesn’t seem to apply to pointers.

What we want is:

fun pget (pp: &usctr, i: int) : char {
var p = *pp;
def var ch, p= get (p,i);
ignore (p); // forget
return ch;
}

but where & is replaced by some reference making operation that requires
the reference to be dereferenced with some operation replacing *,
such that the resulting unique value can be used exactly once. Or to put it
another we we want to write:

var p = ucstr(“Hello”);
char ch = get (p, i);
// p remains live here


where the appearance of p is not considered a use. The address hack does all this,
but it can be abused:

var p = ucstr(“Hello”);
var q = *&q; // cheat makes a copy

In the Haskell example I’m looking at, there is a constructor “lin” for linear types.
Like unique types that have to be used exactly once. However the contract
is different. There’s no promise when making a standard type linear that
there aren’t copied of it. Instead, the user of the linear type makes the same
promises as for a unique type. The linear copy cannot be duplicated or forgotten,
same as for a unique type, but there’s no assurance there isn’t another copy
of the pointer somewhere. The use shown is like this, translated to the char array
case:

var p = someCstring;
var lp1 = linear (p);
var lp2 = linear (p);
linear_set (lp1, “x”, 1);
linear_set (lp2, “y”, 2);
return p;

Here, we make two linear copies of the char pointer, and do two mods
with linear_set which them just forgets its input pointer. The original pointer
is then returned. lp1 and lp2 got used exactly once and forgotten, not
deleted. But this example is as broken as the Haskell one because
the linear_set procedure modifies something knowing there may
be copied of it. It really not clear to be how to use linearity to advantage.
One has to remember Felix, unlike Haskell, has both pointers and mutation.
In Haskell linearity/uniqueness is added to permit mutation, since otherwise
Haskell doesn’t allow it: everything is by default shared but immutable.

But to be clear the point is “linear” qualifier is that it can be applied
to assure linear use of THAT copy, but there is no assurance there isn’t
another copy. So you can’t safely write a “free” of a linear value. Its not
clear why a mutation should be allowed either.


—
John Skaller
ska...@internode.on.net

[John Skaller2]

There is a critical bug in Xcode 11, which can be worked around by

export MACOSX_DEPLOYMENT_TARGET=10.14

This means Catalina CANNOT be targetted. The bug is somewhere in clang, the linker,
or something else and results in a segfault with

(lldb) disassemble -p
libdyld.dylib`stack_not_16_byte_aligned_error:
-> 0x7fff645e22be <+0>: movdqa %xmm0, (%rsp)
0x7fff645e22c3 <+5>: int3
0x7fff645e22c4 <+6>: nop
0x7fff645e22c5 <+7>: nop

Curses on Apple. The bug was known before release.

DO NOT UPGRADE TO CATALINA.

I already did unfortunately. Felix will NOT build on Catalina unless the bug is worked around.
It can also be worked around by not using -O2 but that’s built in to the flx plugin sources.

It seems gcc has the same problem so the bug is possibly in the linker. The bug is NOT
in the Felix generated code. Ordinary C programs crash too, even statically linked ones,
because on OSX the C library is ALWAYS dynamically linked (it cannot be static linked).

—
John Skaller
ska...@internode.on.net

[John Skaller2]

Functional programming is all wrong. I have known this for ages but finding the
correct model is not so easy, and implementing it is even harder :-)

The problem with FP is easy to see: some operations such as division require TWO
exits. Encoding this in a variant does NOT solve the problem because packing the two
internal control paths into a variant type because functions must have a single control
exit with a single fixed return type immediately requires the caller to unpack the data
into two control paths again.

fun div (int x, int y) => match y with
| 0 => None
| _ => Some (x / y)
;

fun sq (r : opt[int]) => match r with
| None => None
| Some z => Some (z * z)
;

fun sqrcp (y:int) => sq ( div (1, y) )

In fact this is all no good, all the math has to be done with opt[int], and that too is no good,
because that encoding only accounts for one possible issue: division by zero. There are other
cases where the “functions” are in fact partial functions, such as taking the square root of
a negative number, and less obviously, representation limitations lead to overflow, etc.

Using a Monad doesn’t solve the problem either. It allows automating the wrong solution,
namely threading. Threading fixes the result type to be the so-called normal result and
adds cases for each type of error. But it still does not and cannot ever possibly account
for where the error occurred.

Throwing an exception restores the ability to write simpler code, but it is an even worse
solution because there is no static coupling between the throw and catch point. We have to dismiss
this as an idea instantly as the garbage that it is. Exceptions are utter rubbish.

The existence of multiple cases for results is NOT EXCEPTIONAL. The use of functions is
simply WRONG. Almost NO operations in computing are functional. Not even integer negation
is a function!

Felix offers a high level solution to this problem using coroutines and synchronous channels.
With a coroutine you read what would be a function argument and write the result. But the key
point is that there can be more than one output channel. There is no need to pack the result of
the computation into a variant and unpack it at each step, then repack it with the output
of the next step, when control bifurcates it stays split unless explicitly rejoined.

The KEY factor in the correctness of this model is that the “normal” and “exceptional”
results are treated symmetrically. Both use the same machinery, channels. This is vital
for more complicated cases. In the functional model there is a thing I will call an
UNFUNCTION for fun. Its more usually called pattern matching. Patterns allow combination
of multiple variants by nesting and help alleviate the problem.

If you don’t understand how powerful patterns are, just try emulating what they do with
functional techniques. This is really driven home in seriously ugly unreadable languages
like Scheme and C++. Patterns draw multiple variations together into a single branch,
so they’re dual to functions in the sense that functional results split control and reify it into
variant data types, whilst patterns merge the variants back into a lesser number of
branches.

However, these are high level solutions. Coroutines are non-trivial. We need a simpler
basis for computing, and the answer is routines. These are what assembler programmers
always wrote and so this is NOT a new solution, rather, its the oldest one!

A routine is a computational unit which accepts arguments but never returns.
Instead, it is passed one or more routines as arguments, and exits by calling
those routines: technically calls are always tail and so are jumps.

The routines which are passed are not raw addresses, but closures. There are two
levels of closing. The main level is binding the routine to its local environment.
A secondary level is obtained by binding the arguments to its parameters.
At this point, the secondary closure is a continuation, ready to run.

A goto is a routine exit which is a short hand (syntactic sugar) for calling
a routine which accepts only a unit argument. So

goto label;

really means

jump label ();

Sequential control flow is also a shorthand, writing

A; B;

really means calling A, passing B as an argument, when A completes,
it jumps to B, passing unit argument. Subroutine calls done like so:

f (g x)

actually means to call g passing x and also f. When g is done f is called
passing the result as an argument.

What we have now is backwards programming. Instead of starting at the beginning and eagerly
executing code, with bifurcations in the control paths based on decisions, until we reach one
or more exits, instead we start at the final result, and work backwards, passing the final calculation
as a routine closure to the previous step. That step calculates the final steps argument as its
result and then passes it to the final step.

In principle this is lazy evaluation. At each point, the “rest of the program” is passed as an argument
to each routine which calculates the argument required for its final closure, binds it to the
“rest of the program” routine to obtain a ready to run suspension, and then runs it. Control still
flows forward, but the programmer has to start by writring the final routine, and work backwards
writing the routines which accept that final routine as an argument, and then, the steps which preceed
them.

Although this seems tricky, and the number of arguments being passed is increased every level
back we go, this is not the usual case. Normally, we don’t actually have to pass the routine used
to exit another because it is known. This is clearly the case for sequential control flow, and indeed
for any goto with a statically known argument.

If you examine a C program almost all the calls and all gotos are to constants. Occasionally,
a function pointer is used, but not often! So with such a program and syntactic sugar,
the resulting program looks .. well it looks the same!


—
John Skaller
ska...@internode.on.net

[John Skaller2]

In respect of

https://ncatlab.org/nlab/show/linear+logic

section 5, game semantics. I believe there is an interpretation for coroutines (possibly elevated
to processes). I’m not sure.

Consider a coroutine with one output channel. There are three possibilities:

1) the routine skips the write operation and terminates
2) the routine attempts to write but blocks
3) the routine writes and succeeds, then terminates

For reading, its symmetrical except was say a read starves rather than blocks.

If a reader and writer are not connected, I/O cannot succeed.
If they are connected, what happens is coupled as follows:

1) The reader and write both skip I/O and terminate.
2) The reader and writer both do I/O and succeed. (Failure is not possible)
3) If the writer skips I/O and the reader reads, it starves
4) if the reader skips I/O and the writer writes it blocks.

####

The game interpretation is:

• In ⊤, it is their turn, but they have no moves; the game never ends, but we win.
• Dually, in 0, it is our turn, but we have no moves; the game never ends, but they win.
• In contrast, in 1, the game ends immediately, and we have won.
• Dually, in ⊥, the game ends immediately, and they have won.

for the connectives:

The binary operators show how to combine two games into a larger game:

• In A&B, it is their turn, and they must choose to play either A or B
• Dually, in A⊕B, it is our turn, and we must choose to play either A or B
• In A⊗B, play continues with both games in parallel. If it is our turn in either game, then it is our turn overall; if it is their turn in both games, then it is their turn overall. If either game ends, then play continues in the other game; if both games end, then the overall game ends. If we have won both games, then we have won overall; if they have won either game, then they have won overall.
• Dually, in A⅋B, play continues with both games in parallel. If it is their turn in either game, then it is their turn overall; if it is our turn in both games, then it is our turn overall. If either game ends, then play continues in the other game; if both games end, then the overall game ends. If they have won both games, then they have won overall; if we have won either game, then we have won overall.

So we can classify things as follows:

• In a conjunction, they choose what game to play; in a disjunction, we have control. Whoever has control must win at least one game to win overall.
• In an addition, one game must be played; in a multiplication, all games must be played.

Other than the decisions made by the player in control of a game, all moves are made by transmitting resources.
Ultimately, these come down to the propositional variables; in the game p, we must transmit a p to them, while they must transmit a p
to us in p⊥

A game is valid if we have a strategy to win (whether by putting the game in a state where we have won or by guaranteeing that it is forever their turn).

####

So starting at the end, a game p is a write, and p⊥ is a read. Being “in control” of the game literally
means the coroutine is running, i.e. has control.

The two conditions & and ⊕ both mean a traditional boolean choice of one control
path or another (& for the writer and ⊕ for the reader). These are the additive connectives,
as in “sum type”. The interpetation A⊗B and A⅋B is a spawn, so now there are two coroutines
both of which can be scheduled.

now the interpretation rests on the constants. The constant 1 represents the writer terminating.
The constant 0 represents the writer blocking.

The constant ⊤ is the reader starving.
The constant ⊥represents the reader terminating.

A game is won if a coroutine has control and terminates.

Actually we don’t care about winning! In Felix, starving and blocking
are both terminal in the sense the fibre is reaped by the GC.

The idea of the calculus here is to reduce expressions representing fibre states to terminals.
The use of dual sets of symbols allows us to track which fibre, the reader or writer, has control.

When the state of the system is A, and the scheduler swaps control from the writer
to reader the state of the system is then A⊥, so negation represents control exchange.

I am not sure of the interpretation yet, however the validity condition is important.
It is basically a way to prove correctness.

Basically its correct if the writer terminates, either by skipping a writer or doing one
successfully, OR, it blocks BECAUSE the reader starves. But if the reader simply
skips a read and the writer blocks, the coupled coroutines are invalid.

Anyhow the IMPORTANT thing is the semantics appears to justify my insistence
that Go is a heap of crap because it gets the termination semantics wrong.
Felix gets the right. It is NOT an error to starve or block, provided the fibres
are unreachable they run forever in principle but this is optimised by the GC
reaping them.

Note we’re dealing with one-shots here, not the usual loops. Note also that
when a read or write actually starves of blocks, the fibre cannot be scheduled.
Reads and writes always deschedule a fibre until a matching write or read
(on the same channel).


—
John Skaller
ska...@internode.on.net

[John Skaller2]

There are some serious problems with uniqueness types. The killer, and its a total killer,
is that polymorphic functions must be linear, just in case the argument type turns
out to be unique.

This can be fixed by overloading EVERY polymorphic function, which is just not on.
I don’t know how to fix this at the moment.

HOWEVER I am adding linear functions to Felix, starting with linear function types.
The notation is stolen from the linear Haskell proposal:

D ->. C

and for effectors:

D ->.[E] C

and of course 0 is still being used for procedures which can also be linear.
A linear function promises to use its argument once, the argument can
always be unique or non-unique for this reason.

Linear functions are subtypes of non-linear ones. The test case is:

// HOFs
fun hofs (g: int -> int) (x:int) => g x;
fun hofl (g: int ->. int) (x:int) => g x;

fun h (x:int) => x * x; // nonlinear
fun k (x:int) => 2 * x; // linear
var lk = C_hack::cast[int ->. int] k;

println$ hofs h 42;
//println$ hofl h 42; // should fail

println$ hofs lk 42;
println$ hofl lk 42;

There is currently no way to define a linear function, so we have to form a closure
of a function with ordinary function type, and cast it to a linear function. I’ll fix this later.

The test is checking subtyping rules: if the HOF accepts a nonlinear function, you should
be able to provide a linear one as well. If it accepts only a linear function, a nonlinear
argument should fail with a type error.

Functions of linear type work exactly the same as nonlinear ones otherwise.
The composition rule is that a composite of linear functions is linear otherwise composites are nonlinear.
This isn’t checked yet.

—
John Skaller
ska...@internode.on.net

[John Skaller2]

This now works:

//////////

// HOFs
fun hofs (g: int -> int) (x:int) => g x;
fun hofl (g: int ->. int) (x:int) => g x;

fun h (x:int) => x * x;

fun k (x:int) =>. 2 * x;

println$ hofs h 42;
type-error println$ hofl h 42; // should fail

println$ hofs k 42;
println$ hofl k 42;
//////////

Here we have our first way of defining a linear function using =>. in a short form function definition.


—
John Skaller
ska...@internode.on.net

[John Skaller2]

Felix now handles linear lambdas and linear function composites.
Still no checking.

Linear functions generate the same code as nonlinear ones at the moment.
I plan to change this, in fact I only made the rule above to get stuff working.

Basically a C++ linear function type will be derived from the
nonlinear function type it is a subtype of (with a trivial derived class
with no content). This will enforce the subtyping at C++ time as well.

Note also not all function forms can be linear at the moment.
In particular the fun f(..){ .. } form and the fun f: D -> C = .. form
can’t be linear yet.

Note I’m still confused about

match uniqval with | pat1 => expr1 | pat2 => expr2 ..

There are two problems:

(a) uniqval is inspected by every pattern until one matches which
is hardly “use exactly once”

(b) A tuple inspection like (v1, v2) is equivalent to two assignments:

val v1 = prj 0 uniqval
val v2 = prj 1 uniqval

which again uses the uniquval twice. In linear logic there are
acually TWO products:

* Tensor product (multiplicative)
* Additive product (additive)

With the tensor product the explanation is “you can apply either the first
or second projection but doing so kills the value so you cannot get both
components out”. Smacks of Heisenburg in quantum mechanics,
and with good reason: linear logic is a variant of quantum logic.

The additive product & allows you get both values out provided you do it
simultaneously. Pattern matching “in principle” does that.

Note there is a correlation pointed out that tensor product is intrinsically
lazy evaluation, whereas the additive product is eager (I think from memory
of the paper).

In any case, whilst looking at the theory, in Felix the rules are exclusively
based on the contract programming paradigm.

Anyhow here’s the current test case .. it remains to be seen if linear functions
are actually useful.

/////////////////////
// HOFs
fun hofs (g: int -> int) (x:int) => g x; //nonlinear
fun hofl (g: int ->. int) (x:int) => g x; //linear

// named functions
fun h (x:int) => x * x; //nonlinear
fun k (x:int) =>. 2 * x; //linear

// linear lambda
var j = fun (x:int) =>. 2 * x;

// composite
var k2 = k \circ k; // composite of linear functions is linear

// Apply nonlinear hof to nonlinear function
println$ hofs h 42;

// Apply linear hof to nonlinear function

type-error println$ hofl h 42; // should fail

// apply nonlinear hof to nonlinear function
println$ hofs k 42;

// apply linear hof to linear function
println$ hofl k 42;

// apply linear hof to linear lambda
println$ hofl j 42;

// apply linear hof to linear composite
println$ hofl k2 42;

// apply nonlinear hof to nonlinear lambda
var ff = fun (x:int) => x + 1;
println$ hofs ff 88;

// apply nonlinear hof to linear lambda
var gg = fun (x:int) =>. x + 1;
println$ hofs gg 88;

// apply nonlinear hof to linear lambda
println$ hofs gg 88;
/////////////

—
John Skaller
ska...@internode.on.net

[John Skaller2]

Hmmm …

This code:


fun bad (zz:int) =>. zz * zz;
println$ "Bad " + (bad 7).str;

Should make the uniqueness checker barf. But it happily says:

Once check examining linear function bad
** Calculated fairy variables, ix2chain index=
65647 -> zz<64295>
Once_check: Detected once variable of function bad
instruction return apply(*<6906>closure[int], (zz<64295>varname, zz<64295>varname));
GETS: (65647:->zz)
Calculated once use per instruction of bad:64293
0@46 return apply(*<6906>closure[int], (zz<64295>varname, zz<64295>varname));
0@46 ()
flow: function return
flow: analysis done ***************

So I tried this:

fun badold (zz: uniq int) => zz * zz;
println$ "Old bad " + (badold 7.box).str;

and that passed too. So there’s a bug. The uniquely typed variable zz is used twice.

I hacked the compiler so in the linear function case “bad” the parameter type is also uniq int.

So I’m pretty sure what’s happening without examining the code, is that the routine is doing
control flow analysis, and will correctly detect if I read a dead variable or write a live one.

But the state changes with control flow, two reads in an expressions aren’t distinguished from
one read (or three .. but they are from zero).

So here’s the problem: this code:

let rec find_once bsym_table (chain2ix:chain2ix_t) path (b:BidSet.t ref) e : unit =
match e with
| BEXPR_varname (i,_),_ ->
let prefix = List.rev path in
List.iter (fun ((j,path),ix) ->
if j = i then
if Flx_list.has_prefix prefix path then
b := BidSet.add ix !b;
)
chain2ix

| BEXPR_apply ( (BEXPR_prj (n,_,_),_), base ),_ ->
let path = `Tup n :: path in
find_once bsym_table chain2ix path b base

| x -> Flx_bexpr.flat_iter ~f_bexpr:(find_once bsym_table chain2ix path b) x

Finds “gets” in an expression: a “get” is just a variable name. The complexity here
is that Felix handles a variable of tuple type as a collection of “fairy” variables.
A fairy variable consists of the variable itself, or, recursively, a component of the
variable located by a list of projection indices, 0 for the first projection, 1 for
the second projection, etc.

A “set” is detected by instructions assign, init, and storeat, its basically the same idea.
In particular it’s very beautiful that the ONLY way to store a value in a variable or
a component of a variable is to use a pointer to the variable or a component,
recursively, thereof, so the algorithm is basically the same for gets and sets.
The only trick is that only a store of the form “storeat (&x, v)” is detected, that is,
the variable name being stored to must be directly in the first argument of the
store instruction. If the address is taken externally, the compiler can’t know
which variable it is the address of. Aliasing problem. Of course the same applies
to gets, where we’re dereferencing a pointer.

The PROBLEM is quite clear. For any expression we’re adding the get or set
to a BidSet, which is just a set of (fairy) variables.

So if there are one, two, three, or more gets in an expression .. only one entry
is made:

b := BidSet.add ix !b;

—
John Skaller
ska...@internode.on.net

[John Skaller2]

> On 20 Jan 2020, at 12:58, John Skaller2 <ska...@internode.on.net> wrote:
>
> Hmmm …
>
> This code:
>
>
> fun bad (zz:int) =>. zz * zz;
> println$ "Bad " + (bad 7).str;
>
> Should make the uniqueness checker barf.

Flx_once: Duplicate Get variable zz in apply(*<6906>closure[int], (zz<64295>varname, zz<64295>varname))
Instruction return apply(*<6906>closure[int], (zz<64295>varname, zz<64295>varname));
/Users/skaller/felix/tlin.flx: line 46, cols 3 to 32
45:
46: fun bad (zz:int) =>. zz * zz;
******************************
47: println$ "Bad " + (bad 7).str;

Uniqueness Error in function bad
ERROR in uniqueness verification phase Polymorphic


Now it barfs! :-)

—
John Skaller
ska...@internode.on.net

[John Skaller2]

Wow. I like it:

Flx_once: Duplicate Get variable x in (x<14579>varname[<T14577>], apply(copy<14564>closure[<T14577>], apply(unbox<9174>closure[list[<T14577>]:TYPE], x<14579>varname[<T14577>])))
Instruction return (x<14579>varname[<T14577>], apply(copy<14564>closure[<T14577>], apply(unbox<9174>closure[list[<T14577>]:TYPE], x<14579>varname[<T14577>])));
/Users/skaller/felix/src/packages/lists.fdoc: line 188, cols 3 to 80
187: fun copy[T] (x:uniq list[T]):uniq list[T]=> x;
188: fun dup[T] (x:uniq list[T]):uniq list[T] * uniq list[T] => x, copy (unbox x);
******************************************************************************
189:

Uniqueness Error in function dup

ERROR in uniqueness verification phase Polymorphic

It’s right. x occurs twice. The idea was to return the original list AND
a fresh copy of it. But the encoding should be:

let u = unbox x in
box u, box (copy u)

where copy u copies the list u, or just copy u, depending on what I happened to
use as the return type.

—
John Skaller
ska...@internode.on.net

[John Skaller2]

I have to consider the very ugly solution to the polymorphism problem.

Recall a normal polymorphic function like this:

fun dup[T] (x:T) => x,x;

passes type checking, passes early uniqueness checking, but will
fail SOME uniquness checks if for example T is set to uniq X,
and pass others.

We CANNOT allow polymorphic code that sometimes works and sometimes doesn’t,
that’s C++ rubbish of the kind that Felix was specifically designed to avoid.
That kind of thing destroys parametricity.

The ONLY solution is to ban instantiation a type variable T with a type X,
where X is uniq U, or, X contains some uniq in a nasty place somewhere.
So X can’t be a product of any kind with a uniq component, but there
are probably more cases.

If you actually want a unique type, you have to write

uniq T

where T isn’t unique (or contains a uniq as above).

However if we have a function

fun linear[T] (x:T) =>. ...

which is linear, T could be uniq, or contain a uniq, harnlessly.
On the other hand, if the T is part of the parameter, not at the top
level, this won’t work.

My conclusion is that embedding uniqueness types in a language where
the default is sharing cannot work. It must be done the other way.

—
John Skaller
ska...@internode.on.net

[John Skaller2]

>
> My conclusion is that embedding uniqueness types in a language where
> the default is sharing cannot work. It must be done the other way.

However embedding linear functions works fine!

The problem is trivial: D ->. C is a subtype of D -> C.
However uniq T is a subtype of T. What we actually require
is that T is a subtype of shared T. In other words a type variable
alone is unique. That we polymorhic functions with parameter type T must
treat the parameter as unique. If by chance we give shared X as the instance
it still works. If we want a polymorphic function that does sharing we have
to explicitly use the type shared U.

—
John Skaller
ska...@internode.on.net

[John Skaller2]

I need to say this another way. If a type variable is unique, then

var x: T

is unique. To make a variable shared we write:

var y: shared T

If by chance we replace T with shared X we get, respectively:

var x: shared X
var y; shared (shared X)

Since x was used uniquely, no harm is done is it is actually shared.
The double shared is ugly but could be collapsed to just shared.

So the author of a polymorphic function has CONTROL of the situation.

At present, if you write

var x : T

the variable has to be treated as unique, and there is NO WAY TO
SAY THAT y is shared.

The best we can do is overloading:

fun f[T] (x:uniq T)
fun f[T] (x: T)

The second function can assume x is shared because if it were unique the first
function would be called.

Now the point is, when you implement a particular polymorphic algorithm
it should work for all T. If a variable is treated as unique by the algorithm,
give it type T: the algo will still work even if it is shared. On the other hand,
if you need a shared variable x in the algo, give it type shared T.

So for any algo, you can always write the type, if we use shared combinator.
If we used uniq combinator, as Felix does now, we’re screwed.

You can embed shared types in a linear type system, but the converse
is not possible.


—
John Skaller
ska...@internode.on.net

[John Skaller2]

>>> My conclusion is that embedding uniqueness types in a language where
>>> the default is sharing cannot work. It must be done the other way.
>>
>> However embedding linear functions works fine!

There’s a way to do it,

Let *linear* be all types including uniq ones and *shared* be types
not involving “uniq”, so shared types are copyable. Types like

uniq int * int

are not copyable. Similarly any variant constructor with uniq in it
implies he variant isn’t copyable. Linear functions

A ->. B

however are just a subset of ordinary functions represented by
pointer so are copyable, even if A or B are not, indeed, A -> B
is copyable. So the rule isn’t quite right “not involving uniq”.
I think it only applies to sums and products.

—
John Skaller
ska...@internode.on.net

[John Skaller2]

Grrr. This doesnt work:

fun dup[T] (x:uniq list[T]):uniq list[T] * uniq list[T] => let y = unbox x in box y,copy y;

Felix thinks x isn’t used. The reason is that let x = y in z is desugared to:

fun mf () {
match y with
| x => z
endmatch
}
return mf();

So dup is given by:

fun dup (x) {
fun mf () {
match unbox x with
| y => box y, copy y
endmatch
}
return mf ();
}

Now, x is indeed used in mf, a child of dup. I think the problem is, the application
is of closure mf to (). The actual match check function is known to be true, so dropped,
so there’s no conditional to cause a problem. The code goes to:

fun dup(x) {
fun mf() {
y = unbox x;
return box y, copy y;
}
return mf();
}

However the actual debug print shows this:

return explicit_coercion((dup_mf_3593<3593> ()):>>uniq list[T] * uniq list[T]);

In particular THIS encoding works fine:

fun dup[T] (x:uniq list[T]):uniq list[T] * uniq list[T] {
var y = unbox x;
return box y,copy y;
}

The problem I think is that Felix assumes nested functions cannot change the liveness state
of a parent variable. The can’t assign to one, that would be a side effect. But reading
one also has an “effect”.

This logic doesn’t apply to procedures. Felix tracks direct calls, but not calls through
expressions (that is, closures), because obviously, it doesn’t know which procedure
was used to form the closure.

I’m going to leave this for a moment.

—
John Skaller
ska...@internode.on.net

[John Skaller2]

OK, so this is what I’ve done.

There is a new kind LINEAR which is the top level universal kind of type expressions which
describe run time values.

The previous top level, TYPE, is a subkind of LINEAR.

Types of kind LINEAR may or may not be copyable.
Types of kind TYPE are always copyable.

It’s a bit counter intuitive, however the compiler is littered with TYPE defaults.
If a type variable is not given a kind it defaults to TYPE as before.

The reason for these choices is thus to ensure polymorphic algorithms like:

fun dup[T] (x:T) => x,x;

continue to be correct polymorphically after the addition of uniqueness types.
If you call

dup (uniq int)

T would be deduced to be uniq int, which is LINEAR but not TYPE,
that is, its a run time type which can be moved but not copied.
So the call fails (with a confusing “can’t find dup” error).

The notation is justified in the sense that linear logic calculi embed
intuitionistic logic using a special operator. Felix does it the other
way around. In a polymorphic linear logic a type variable would have
to be linear if introduced outside the embedded sharable subexpressions.

In other words, sharable is a subkind of linear, so not copyable is
actually linear minus shared.

If you want to allow uniq X as an instance of a type variable you have to
explicitly add the kinding annotation LINEAR:

fun swap[T:LINEAR,U:LINEAR] (x:T,yU): U * T => y,x;
var a,b = swap (box 1. 2);

Now, b = box 1, and a = 2. If you leave off the LINEAR for the first
type, the call should be rejected becuase T would default to TYPE
and uniq int isn’t a TYPE because it isn’t copyable.

There’s no easy way to say “LINEAR but not TYPE”, although I think you can
say it in a complicated way. I may need to fix this. However I am leary at the moment
of having more than one way to express a kind, since then checking constraint
matching would require reduction rules and open many cans of worms which
I plan to open later when I know the new worms cause problems, not old caterpillars..

Now, what is CONFUSING is that uniq X is a subtype of X, but the kind
of uniq X is LINEAR which is a *supertype* of the kind of X, which is
defined as TYPE.
================
There are now some issues. You can box any value, or use the uniq
function (type constructor _uniq) on any type. You can even get
uniq (uniq (uniq thingo)). We could flatten it, so uniq is idempotent,
that is, so uniq (uniq X) = uniq X. That makes uniq X a fixpoint of
uniq, for all X. We could also make unbox of a non-boxed type
just return the type, so that unbox X where X not boxed is just X.
However unbox would not be idempotent unless box was,
which would ensure there was one level of boxing possible,
at least without an intervening wrapper type.

BTW: clearly “void” type is not copyable. Actually its not movable either.
So perhaps there is another kind ANY which is above even LINEAR,
of which the type “top” is the only element that is not linear.
And perhaps there’s a VOID kind which has only type void in it
at the bottom. So the lattice has top and bottom.

The problem here is the known problem that functions returning
void are considered procedures. But void is bottom, it should
really be top. Note FPLs use unit which is just as wrong:
a function returning unit is useless. A function accepting unit
is a way for an eager language to support closures, nonsense
in a lazy language though (no need to suspend a computation,
since they’re all suspended until required anyhow).


—
John Skaller
ska...@internode.on.net

[John Skaller2]

Finally, the first real problem.

[Flx_lookup.bind_expression] Inner bind expression failed binding (lhs, (append ((deref lhs), rhs)))
CLIENT ERROR
[flx_bind/flx_lookup.ml:2973: E149] [lookup_name_with_sig]

Can't find deref[] of
BTYP_ptr(RW,BTYP_uniq(BTYP_inst(18521[]:TYPE)),[])
=
deref[] of RWptr(uniq((_ustr)),[])

In /Users/skaller/felix/src/packages/ucstring.fdoc: line 410, cols 20 to 24
409: proc += (var lhs: &ustr, var rhs: ustr) =>
410: lhs <- append (*lhs,rhs)
*****
411: ;

where:

fun _deref[T]: &<T -> T = "*$t";
fun deref[T] (p:&<T) => _deref p;

Now a RW pointer is a subtype of a RO pointer (RW=read/write, RO=read only)
with the same type. But there’s a special case because a uniq T is also a subtype of T,
so the unification engine has a nasty hack which allows both subtyping rules to be
applied simultaneously: a RW pointer to a uniq T is a subtype of a RO pointer to T.

Well actually .. I’m wrong: the code in the unification engine is:

| BTYP_ptr (`W,t1,[]), BTYP_ptr (`W,BTYP_uniq t2,[])
| BTYP_ptr (`W,t1,[]), BTYP_ptr (`RW,BTYP_uniq t2,[])
(*
| BTYP_rref t1, BTYP_rref (BTYP_uniq t2)
| BTYP_rref t1, BTYP_pointer (BTYP_uniq t2)
*)
-> add_eq (t1,t2)

so actually the read case is comment out. Felix won’t work without the write hack though.
The write hack says a write only pointer to T1 also accepts a write pointer to uniq T2 and
a read/write pointer to a uniq T2, provided T1=T2, so no variance is allowed in the T.

The read case is comment out but used to work. The logical conclusion is that the T
in deref needs to be annotated LINEAR!

Fixing that I get:

ClientError Whilst calculating return type:
[flx_bind/flx_cal_ret_type.ml:159: E105a] [cal_ret_type2] Inconsistent return type of deref<5583>
Got: BTYP_type_var(5583:TYPE)
= <T5583>
And: BTYP_type_var(5584:LINEAR)
= <T5584:LINEAR>

So this is one of those cases where I’m guessing or hacking the return type as a type variable
of kind TYPE, when the actual return type is of kind LINEAR.

Cool, fun problem!

—
John Skaller
ska...@internode.on.net

[John Skaller2]

> On 25 Jan 2020, at 02:57, John Skaller2 <ska...@internode.on.net> wrote:
>
> Finally, the first real problem.
>
> [Flx_lookup.bind_expression] Inner bind expression failed binding (lhs, (append ((deref lhs), rhs)))
> CLIENT ERROR
> [flx_bind/flx_lookup.ml:2973: E149] [lookup_name_with_sig]
>
> Can't find deref[] of
> BTYP_ptr(RW,BTYP_uniq(BTYP_inst(18521[]:TYPE)),[])
> =
> deref[] of RWptr(uniq((_ustr)),[])

So, I know what’s going on:

+++++++++++++++++++++++++++++
Cal ret type of deref<5583> at /Users/skaller/felix/src/packages/pointers.fdoc: line 37, cols 3 to 43
+++++ UNBOUND return type is <var 5583>
RETURN TYPE UNSPECIFIED
Flx_cal_ret_type: function return type from SYMDEF bound as BTYP_type_var(5583:TYPE) = <T5583>

ClientError Whilst calculating return type:
[flx_bind/flx_cal_ret_type.ml:159: E105a] [cal_ret_type2] Inconsistent return type of deref<5583>
Got: BTYP_type_var(5583:TYPE)
= <T5583>
And: BTYP_type_var(5584:LINEAR)
= <T5584:LINEAR>

The “UNSPECIFIED” test is this Ocaml:

begin match rt with | `TYP_var j when j = index -> print_endline ("RETURN TYPE UNSPECIFIED") | _ -> () end;

What happens is, if the return type of a function is not specified, which is originally indicated
by the typecode `TYP_none, then when Felix puts the function in the (unbound) symbol table
it sets the return type to

`TYP_var k

where k is the function symbol index. This is a trick! There’s no such type variable.
Once the return type is established, during binding, a cache of function return types
is created mapping the function index to the actual return type, as well as putting
the actual return type in the bound symbol table.

The use of these phantom type variable is crucial during binding, because it allows
binding the return type of recursive functions and other functions whose return
expressions call the function we’re working on. The bound type is incomplete in the
sense it may contain the dummy variable.

This is a standard technique. It is the basis of type inference. What we do is as we go
along we use unification to refine the type the type variable maps to. Hopefully
when the whole program is bound, all the phantom type variables have been
reified to type expressions not containing any phantoms: this is precisely what
unification does.

The PROBLEM is that this is all fine if we know the kind of the type variable.
We used to just say TYPE was the kind. But deref now has a type variable
of kind LINEAR.

Unification would be correctly saying that the phantom (index 5583) is set to the
function polymorphic type variable (index 5584) BUT the problem is that
type variable has kind LINEAR, whereas the phantom only has kind TYPE.

Now, the RIGHT way to do this is to give the phantom the kind KIND_var ix,
where ix is a fresh integer, that is, to introduce kind variables. Then, we can
use unification to find the kind variable. But we don’t have kind variables.

The actual unification engine, however, DOES take account of subkinding
rules if the type variable indicies are distinct. The Ocaml is too long to show,
but a type variable of kind LINEAR can be set to a type of a kind which is
a subkind of LINEAR. But the phantom has kind TYPE and the argument
type has kind LINEAR, which is backwards.

A solution is just to declare the return type.

But a BETTER solution is to change the phantom to have kind LINEAR.

The argument is if the return type were of kind UNITSUM, it already works
with phantom of kind TYPE, so the subkinding stuff works already, we just
didn’t pick the maximal kind. Its nice to have a theory that something must
work because it already does.

And .. it worked!!!!

HOWEVER this still works and should fail:

fun f[T:TYPE] (x:T) => 2;
println$ f(box 1); // should fail

If I replace TYPE with UNITSUM it fails as expected. So there’s some kind of
check somewhere that’s not finding that uniq int is not a member of kind TYPE
(but does find it isn’t of kind UNITSUM).


—
John Skaller
ska...@internode.on.net

[John Skaller2]

Ooops. I understand the problem now.


fun f[T:LINEAR] (x:T) => 1;

fun f[T:TYPE] (x:T) => 2;

fun f[T:UNITSUM] (x:T) => 3;

println$ f(box 1); // should print 1
println$ f true; // should print 3

I expected the print to print 1 because it best matches case 1.

However the subtyping rules allow a uniq type to be coerced to
a shared type, automatically unboxing it.

Here’s the rule:

(* here we throw away uniq part of argument type passing a value *)
| t1, BTYP_uniq t2 -> add_ge (t1,t2)

Note this is a very specialised rule. It ONLY allows a uniq type to be coerced
to the underlying shared type. For example uniq int -> int.

The unification engine doesn’t rank coercions, in fact it doesn’t even do any
coercions. Instead, it just says the type is a subtype and thats OK, end of story.

When the compiler calculates an application it checks AGAIN of the parameter
and argument types agree. If not, it throws in a coercion of the argument to
the parameter type.

This is safe, because the unification engine already said so. :-)

Because of this, BOTH of the first two f’s above match, and the second
one is chosen becuse TYPE is more specialised than LINEAR.

THE COMPILER IS RIGHT.

Weird eh? So lets try this:

fun f[T:LINEAR] (x:T) => 1;

fun f[T:TYPE] (x:T) => 2;

fun f[T:UNITSUM] (x:T) => 3;

var y = 1, box 1;
println$ f y;
println$ f(box 1); // should print 1
println$ f true; // should print 3

Sure enough, it prints 1,2,3. The type of y is int * uniq int, which has kind
LINEAR but NOT kind TYPE. However, the type is not exactly matching

uniq T

and so the special case recognised by unification is not triggered.
No coercion is done.

To put this another way the subtyping rule gazumped** the subkinding rule!

** gazumping is a nasty practice where a house is for sale and someone
immediately accepts the deal, preventing anyone else accepting it.
Then, during the mandatory cooling off period, they withdraw their offer
and make a new lower offer .. unbeknown to the other parties who were
blocked from making offers because an offer had already been accepted.

SO WHAT TO DO? It seems that according to the rules, surprisingly,
Felix compiler is actually working correctly, and the bug is actually
to be found in my brain.

—
John Skaller
ska...@internode.on.net

[John Skaller2]

> SO WHAT TO DO? It seems that according to the rules, surprisingly,
> Felix compiler is actually working correctly, and the bug is actually
> to be found in my brain.

It’s not really intuitive, disobeys the Principle of Least Surprise.
If it fooled me, it might fool others. [Is there anyone here? ]

The reason for the rule is precisely to allow a uniq type to be used
by a function which only accepts a shared type, without needing
an explicit coercion; the coercion is done implicity, as is the case
for all subtyping rules.

Of particular concern is

.. hey .. why isn’t sdlgui/gui_01,02, and 03 doing any graphics .. the other tests do .. they all used to ..

ah .. so, the hassle is

println$ (box 1);

Its really hard, since print uses str virtual function. It would be a shame if this didn’t work.
But there is a whole library full of functions that otherwise wouldn’t work too,
both monomorphpic and polymorphic.

There’s the related problem:

var u = f x; // result is uniq
var y = u,u; // ERROR

This can’t be solved by subtyping. You have to write

var u = unbox (f x);

which means you have to know the result is uniq. When I made some functions
uniq, lots of places in the library and tools broke, and i had to do exactly
the above to fix it.

The POINT is that it’s only needed for implicitly typed local variables,
it’s not needed for parameters BECAUSE of the subtyping rule.

print is of particular concern because it unpacks tuples automatically using polymorphic recursion.
So for example print (1, box 1) should work! But it doesn’t! However print (box 1) does. Hmm.
But this works:

println$ (1,box 1)._strr;

because _strr it mechanically unpacks its arguments inside the compiler,
rather than plain str which uses library code using polymorphically recursive
tuple polymorphism. Hmm.

—
John Skaller
ska...@internode.on.net

[Shayne Fletcher]

On Sat, Jan 25, 2020 at 1:54 AM John Skaller2 <ska...@internode.on.net> wrote:

 

 [Is there anyone here? ]

Yes 🤗

--

Shayne Fletcher

[John Skaller2]

> On 26 Jan 2020, at 01:08, Shayne Fletcher <shayne.fl...@gmail.com> wrote:
>
>
>
> On Sat, Jan 25, 2020 at 1:54 AM John Skaller2 <ska...@internode.on.net> wrote:
>
> [Is there anyone here? ]
>
> Yes 🤗

Are you sure you’re all there?

—
John Skaller
ska...@internode.on.net

[Shayne Fletcher]

On Sat, Jan 25, 2020 at 12:08 PM John Skaller2 <ska...@internode.on.net> wrote:

> On 26 Jan 2020, at 01:08, Shayne Fletcher <shayne.fl...@gmail.com> wrote:
>
> On Sat, Jan 25, 2020 at 1:54 AM John Skaller2 <ska...@internode.on.net> wrote:
> 
>  [Is there anyone here? ]
>
> Yes 🤗

Are you sure you’re all there?

No.
 

--

Shayne Fletcher

[John Skaller2]

Its been bugging me for ages that record operations are incomplete. So I now added:

var x = (a=1, b=2, b= "hello",c=42.3);
println$ (x getall b);

The operator getall returns all the fields of a record with the given name,
in order, as a tuple.

This was needed for completion of the field operations. For example
to get the second b field, you can write:

(x getall b) . 1

There was no easy way to do this before. You could only do it by removing
enough b’s so that the first one left was second one before:

(x remove b).b

So actually you could do it but is was horrible.

—
John Skaller
ska...@internode.on.net

[John Skaller2]

> > [Is there anyone here? ]
> >
> > Yes 🤗
>
> Are you sure you’re all there?
>
> No.

Lets see who is paying attention. Here’s a Felix test.
What does this program output?

var x = (a=1, b=2, b= "hello",c=42.3);

println$ (match x with | (b=_ | r ) => r)._strr;

Pattern matching is pretty awesome with row polymorphism!

===================================================

Ok, that one was too easy. So here’s one that I don’t think
I can do:

Write a function that can reverse any tuple.

Is it possible?

You will need

* polymorphic recursion with type classes
* virtual types
* AND GADTs.

For sure you cannot do this in Ocaml or Haskell.

The actual question is: what is missing from Felix, if anything,
to make this work?

Felix can already do things you cannot do in Ocaml or Haskell.
When you say

println$ (1,”hello”, 4.2, true);

some very sophisticated front end stuff is used to do it. You saw above
in the first test the use of _strr to convert a record to a string. This is a
generic function provided by the compiler. In other words, it’s not written
in Felix. But converting a *tuple* to a string can be done in Felix using
row polymorphism and polymorphic recursion. The method is the same
as you’d use with C++ templates, using generic overloads to perform
polymorphic recursion.

Here’s the code, actually used, in the library:

First, we need a helper class.

class Tuple[U] {
virtual fun tuple_str (x:U) => str x;
}

The reason for this class is rather stupid. If you have
a virtual function f in a class, and you want f to call itself
on a different type .. aka polymorphic recursion .. you have
problems because the inner most f at the point of call
will be bound, which only gives you ordinary recursion: in

fun f(x:T) = > f (stuff);

the calls to f calls itself, which means stuff has to be of type T
or Felix barfs. You actually want to call f “as seen from the outside”
but it isn’t possible unless you use explicit qualification which means
you need to know the whole scoping environment of f.

The solution to all problems in computer science is to drink
more coffee. In programming, tip the coffee on your keyboard.
That works because Apple will take at least 3 months to get
replacement parts. In the meantime, you just use indirection:

fun g(x:T) => f (x);
fun f(x:T) => g (stuff);

by introducing a helper function. We use tuple_str as our helper.

Now the code is done by template instantiations,
first an inner tuple print that just puts commas in:

instance[U,V with Str[U], Tuple[V]] Tuple[U ** V] {
fun tuple_str (x: U ** V) =>
match x with
| a ,, b => str a +", " + tuple_str b
endmatch
;
}

instance[U,V with Str[U], Str[V]] Tuple[U * V] {
fun tuple_str (x: U * V) =>
match x with
| a , b => str a +", " + str b
endmatch
;
}


Now, the top level, which just puts parens around stuff:

// actual Str class impl.
instance [U, V with Tuple[U ** V]] Str[U ** V] {
fun str (x: U ** V) => "(" + tuple_str x +")";
}

instance[T,U] Str[T*U] {
fun str (t:T, u:U) => "("+str t + ", " + str u+")";
}
instance[T] Str[T*T] {
fun str (t1:T, t2:T) => "("+str t1 + ", " + str t2+”)”;
}

You will notice an ANNOYANCE. You need three overloads,
not two. This is because Felix tuples are constructed with
a “Cons” like operator: if TAIL is a tuple, then Consing a
new value of the front makes a new tuple. That operator
is spelled

head ,, TAIL

The obvious base type, (), does not work. Its a tuple, and so’

x,, ()

is a tuple, right?

Yes indeed, a tuple with 1 value. The problem is, a tuple with one
value in Felix is EQUAL to that value. Its not merely an isomorphism.
Its an equality. So you cannot cons a new element on front, because
x may not be recognised as a tuple.

I said “may not” deliberately: of course, x is an arbitrary value,
so it might just happen to be a tuple! We don’t want to cons a new
element onto x if its a tuple, we want to make a pair, with x as the
RHS, and that’s what we have to do:

1,,2,,3,4

We have to use a pair as the BASE of the induction because
“single element tuples don’t exist”. Actually they do but they’re
equal to the single element. This is a f’ing PITA because all tuplic
polymorphic recursions need to use a pair as the base, and handle
unit separately. But it is worse because it means there are no
arrays of one element .. since an array is just a tuple with all
components the same type.

=================================

So, the way Felix does polymorphic recursion is the same as C++,
except Felix is properly type checked. Haskell can also do polymorphic
recursion, but it us more advanced …

because it is more retarded.

Haskell uses boxing which is really bad stupidity of lame morons that
are still using 1960’s tech. But the advantage over expanded types is
how Haskell can do run time polymorphic recursion. Whilst Felix and
C++ actually expand the code, Haskell can just generate binary for
a single function because all types have a universal representation,
namely a pointer (box).

However this has another advantage: Haskell can also do polymorphism
on dependent outputs. in C++ this is done with typedefs. For example

Container::value_type

Because it uses delayed type checking this bullshit works. In other
words C++ templates are not type checked until they’re monomorphised,
and monomorphisation is just done by lookup and gluing terms in,
in other words its just macro processing.

Felix can do this too. I introduced “virtual types” to do it.

A virtual type is not specified in the class, but is made concrete
in the instance.

The effect is this: you CANNOT do ordinary overloading on a virtual
type because you don’t know the actual type until monomorphisation
is done. But you CAN do polymorphic recursion, in other words,
you CAN call a virtual function on a virtual type, because the instance
isn’t resolved until monomorphisation.

So to reverse a tuple, unlike the string case, the OUTPUT of the
class virtual is no long invariant. In Felix, I had str as shown above
for tuples, and also comparisons! But these only worked because
the result of the function is invariant. To make the output vary
with the input required virtual types.

It’s worse! It doesn’t just require virtual types. It also required GADTS.
The reason is we are BUILDING a value not just decoding one.
To build a tuple we start with a pair of some type:

A * B

and then we need to cons a new head on it:

C ** (A * B) == C * A * B

where the ** constructor is the type of the ,, operator. It real easy to write out
a sequence:

E ** D ** C ** A * B

and extend it, but the output is a single type which has to be built up by a recursion.
So again solve the problem with more coffee and indirection. We have to make
a new type variable of tuple type to pack all the types into so we can prepend
a new head.

Its very hard. Roughly we have to build a function which is not evaluated yet,
that packs more and more things on the left of the base tuple. When finally
the analytical part of the polymorphic recursion is done, we have to
finally unravel that suspended computation.

Its easy to do this stuff with code. But we have to do it with the type system.
Gadts provides the suspensions. virtual types provide the indirection.

but with the extra complication of starting with a pair instead of a unit,
its really hard .. especially since Felix error messages are messy.

Note you CAN do this kind of thing in Haskell: you cannot reverse
a tuple because Haskell doesn’t actually have products: it uses
exponentials instead. [Technically there is no N-functor to create
tuples: the exponential is used to hack it instead. This simplifies
Haskell because the Curry/Uncurry adjunction doesn’t require a
representation. In fact, that is precisely how products are built,
so any implementation is a representative]


—
John Skaller
ska...@internode.on.net

[John Skaller2]

Ah. I just had a brainwave.

Felix has a pointer type

&T = ptr[T]

(and associated read and write pointers but that isn’t the story here .. )

It cannot be NULL, it cannot be increment. It always points to a single object.
Although in bindings I often cheat (the C it replaces can be NULL).

There is also a type

@T = cptr[T] = | nullptr | Ptr of &T

which is actually a variant in the library, which can be NULL. Note that this corresponds
at the representation level with an ordinary C pointer, this is not a coincidence, its a cleverness
in the design of represntations.

Finally there’s a type

+T = carray[T] = new &T

which is also defined in the library, this time as an abstract type, but we cheat
to allow +T to be an incrementable pointer. Which cannot be NULL??

Well, a possibly NULL incrementable pointer would be useful too. However

@(+T)

whilst it exists, would have the wrong representation: its a NULL or,
its a pointer TO a pointer.

Now here’s the thing. +T is incrementable but the result when pointing
to a C array is going to be invalid past the end of the array. We dont
know the array length so the type is dangerous like a C pointer,
which is exactly the intent, to model C pointers.

But here’s the brainwave. What is the representation of a zero length array?

You may think there’s no fixed answer but you would be wrong!
A zero length array in Felix exists, here it is:

()

Remember, arrays are just tuples with all elements the same type.

the idea is that () doesn’t exist, so we don’t care about the representation,
if you end up with one at C level, which can happen, there’s actually
a diagnostic in the compiler back end it had to generate a hack value.

On the other hand POINTERS to unit certainly exist, and the represntation
is NULL.

Therefore the representation of a pointer to a zero length array is NULL.

Therefore,

+T

as a pointer into an array of length N, where N can be zero,
can also be NULL. In fact if the array is length 0, it pretty
much has to be.

So +T can, by logic, already be null. There’s no need to test
every case though!!!!! Its NOT the same as @T where you do.
Because even if the pointer is not null, incrementing it requires
a check on its position in the array *external* to the type.

Hmm. It’s important to note, this is technically the WRONG representation
for a function like:

char *copychars(char const *from, char *to)

where, if “to" is NULL, the function returns a malloc’d array, otherwise
it writes into “to” and returns that, because THAT meaning of NULL
is actually @+T, as opposed to “we gave you a place to write that
was too small” (because that cannot be detected!)


—
John Skaller
ska...@internode.on.net