new kinds

[John Skaller2]

I have added some new kinds to Felix:

COMPACTLINEAR
UNITSUM
NAT
BOOL

I think i need INT as well.

So NAT and BOOL are basically compile time unsigned int and
bools. However do not be confused: they’re not run time values
that happen to be constants the compiler can understand.

A BOOL for example would the result of something like
a type assertion. It might be used for conditional compilation
or erroring the compiler out.

On the other hand, UNITSUM and COMPACTLINEAR are
intended to be subkinds of TYPE. The idea is you can write

fun f[T:COMPACTLINEAR] (x:T) => ….

and constrain the type variable T to a compact linear type.


Why do we need ths kinding stuff????

Well, consider two varrays v1 and v2 then

v1 + v2

is a varray with the concatenated contents of both,
its easy to get the lengths of each, add them together
make a new varray big enough, then push the values
of first v1 and then v2 into it. You do this AT RUN TIME
because the length of a varray is only known at run time.

How would you do this for farrays? That is
compile time arrays like int ^ 4?

Its easy to write a function:

fun cat(x:int^4,int^5):int^9 => ….

and you can make it polymorphic in the base type easily too
but you CANNOT make it polymorphic in the indices because
there is no way to add the lengths of the arrays.

if you look in the library you will find this:

//$ Join two arrays (functional).
fun join[T, N, M] (x:array[T, N]) (y:array[T, M]):array[T, N + M] = {

Of course .. it doesn’t work. The result is NOT an array of length
M+N, because M+N doesn’t do integer addition: its a SUM TYPE.

The problem is, in principle M and N could be ANY types:
the type variables N,M are unconstrained. But here:

fun join [T, N:UNITSUM,M:UNITSUM] … UNITSUMADD(N,M) …

we have hope because N and M are now *known* to be unitsums
and the UNITSUMADD compiler function can add them. The
result is a unitsum, although the actual length is not known
polymorphically, it will be known after monomorphisation,
So te compiler would need a UNITSUMADD term during polymorphic
processing, which is recognised as a UNITSUM kind.

At present, you can write these kinds but it will just either bomb the
compiler or do nothing. Not sure, haven’t tried it :)




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

[John Skaller2]

I have some injections working now.

Injections are the dual of projections.
They’re sometimes (incorrectly) called type constructors.

@felix
// injection: union
begin
union X = | A of int | B of double;
var ia = A of int;
var x = ia 42;
println$ x._strr;
end
@expect
A (42)
@felix
// injection: polymorphic variant
begin
typedef X = (`A of int | `B of double);
// var ia = `A of int;
// var x = ia 42;
// println$ x._strr;
end
@expect
@felix
// injection: sum
begin
typedef X = int + double;
var ia = case 0 of X;
var x = ia 42;
println$ x._strr;
end
@expect
case 0 (42)
@felix
// compact linear sum
begin
typedef X = 3 + 4 + 5;
var ia = case 1 of X;
var x = ia (`2:4);
println$ x._strr;
end
@

The polymorphic variant injections are not workking yet.

More importantly, coarrays aren’t working yet.

WTF is a coarray you say? Well its the dual of an array. :-)

If you have a type

int + int + int

it can also be written

3 *+ int

which means to add up int 3 times. In other words, every sum type
for which all the injection arguments are the same type is a coarray.
There is a term for them in the compiler but at present sums satisfying
the condition are not translated. There is also a second level special
case:

3 *+ 1

which is just the unitsum 3. This is a special compiler term.

The thing about coarrays is like arrays: the injection index can be
dynamic (an expression, not just a constant). Because, the
domain is the same for all injections.

The really fun part is that, as arrays can have structured indicies,
eg you have have int ^ (3 * 4) which is a matrix, so too must
coarray injections have structure repeat counts. The repeat count
isn’t an integer .. its a type. In fact any compact linear type will do,
just as it is for the exponent of an array.

Understanding that is rather much a brain twister.

There’s more. For any tuple type, there is a thing called
a *generalised projection*. The idea is simply that it is a map:

A * B * C -> A + B + C

Because now the codomain is the same for all projections,
it can be dynamically indexed. An array is now a special
case where you can “smash” away the constructor.
however the costructor is useful: if you iterator over an
array with a generalised projection, the output is a logically a pair
consisting of the index and the array value:

A ^ N -> N *+ A


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

[John Skaller2]

At the moment, unique types are hard to use. For example, suppose we
allocate a T on the heap, the returned type should be a unique pointer to T:

box (new v): uniq (&T)

However by the current rules, a function accepting a plain pointer to T can’t
use that type:

proc f (px: &T) …

We have to code a second procedure:

proc f(px: uniq (&T)) { p (unbox px); }

Now, perhaps sometimes, we really want two procedures.
For example, suppose we have a C char pointer and we want to upper case
the underlying chars. If we get a uniq pointer we can do it in place.
If the pointer isn’t uniq, we have to make a copy to modify to preserve
referential transparency.

However, it is safe to do the copy, even if the argument is uniq,
just not optimal. So there is a strong argument that

uniq T is a subtrype of T

With that subtyping rule, we can use a uniq T anywhere a T is expected,
i.e. as an argument.

Thought is required though. Sometimes we do not want referential transparency.
We actually want to share mutations. An example: consider a term in a calculus
to which reductions can be applied. Often, the reduced form has the same semantics
and so there’s no harm sharing semantics preserving modifications.

There is an extremely common example of this: using a cache to speed up
purely functional calculations. In fact functional languages, particularly Haskell,
so this routinely: its call hash-consing for some obscure historical reason.
Given any suspended computation, that is, a closure, we have to evaluate
it “on demand” i.e. lazily. However due to purely functional referential transparency,
once it has been evaluated, subsequent evaluations should produce the same
result. So we can cache the result of the closure evaluation, and use that the
next time the closure is evaluated. Felix doesn’t do this, Haskell on the other
hand almost MUST do it or it would be ridiculously slow, considering
*all* function applications (including constructors) are lazy.

SO: I don’t want to throw the baby out with the bathwater BUT I suspect
it is necessary to make uniq T a subtype of T. In effect a function passed
a uniq T with type T is implicitly unboxing the argument. In theory,
it is safe.

But there’s a problem. Felix doesn’t seem to overload on subtypes.
It always picks the most specialised type, and it uses unification to
detect that *including* subtyping. So why doesn’t it work?

The problem must be in the overload resolution engine.
It performs polymorphic specialisations but not subtyping ones.
That is, it inserts type specialisation by not coercions.

Coercions are inserted AFTER overload resolution is done,
in fact, there is a routine called “cal_apply” that calculates
an application. If the function argument doesn’t agree exactly
with the parameter, the argument is coerced so it does.
Polymorphic specialisation, however, is done by specialising
the function, not by coercing the argument.

For example if you have swap[U,V[ (x: U, y: V): V * U => y,x;
and you do swap (1,”hello”) then the application is

swap[int, string] (1,”hello”)

so tyhat the argument agrees with the specialised function.
But with a subtype,

fun f[D] (x:D) => …
var x : B; // base super type
f x

you’re actually doing this:

f (x:;>>D)

that is, embedding the subtype B in the super type D, so now
the match is exact.

What we *should* be doing is coercing the function, in particular its domain,
not the argument because THEN we can compare signatures to find
the most specialised.

Unfortunately the unification engine doesn’t tell what coercsions are
needed. That is, the output is just a MGU or most general unifier,
but the unifier doesn’t include coercions.


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

[John Skaller2]

Hmm .. this works:

truct A {};
struct B {};
supertype A: B = “$1”; // coercion from B to A, so B is a subtype of A

fun f(x:A) => 1;
//fun f(x:B) => 2;

println$ f #A;
println$ f #B;

prints 1 and 1.

Remove the comment so there’s an overload.
It still works. prints 1 and 2.


Hmmm.

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

[John Skaller2]

> Hmm .. this works:
>
> truct A {};
> struct B {};
> supertype A: B = “$1”; // coercion from B to A, so B is a subtype of A
>
> fun f(x:A) => 1;
> //fun f(x:B) => 2;
>
> println$ f #A;
> println$ f #B;
>
> prints 1 and 1.
>
> Remove the comment so there’s an overload.
> It still works. prints 1 and 2.

HOWEVER when I try to make uniq T a subtype of T all hell breaks loose.
I get a chain of overload resolution errors sometimes, and other times
I am getting a “not found” error on a private function. However the
abstraction mechanism was used and it should work. This occurs
in the unique test case ucstring in the slice handling.

Doesn’t make sense: an ambiguity I can understand. Unfortunately
in the weird case handling, overload failures don’t get reported
as such because they result in chaining to the next weird case.
I just get a chain of overload resolution failures without an indication
WHY the overload failed (not found, or ambiguous?).


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

[John Skaller2]

>
> HOWEVER when I try to make uniq T a subtype of T all hell breaks loose.

Got it!

Felix thinks uniq T = T. The reason is quite obscure: idiot me
didn’t alpha-convert.

recursion in unification, terms: uniq((<T8682>)) = <T8682>
Function domain <T8682> = argument type uniq((<T8682>))

Felix is *solving* for T:

s := Some (i, Flx_btype_rec.fix i t)

by introducing a fixpoint operator. In effect:

T = uniq X as X

What I should be doing is checking if

U > uniq V

and the answer is yes, with U set to V. Now we check

uniq U >= V

and the answer is NO. In both cases the parameter is on the
left, with a dependent type variable U. The variable V is
existential, not universal, that is, it is not variable at all,
its an independent, unsettable, variable.

When doing a unification the usual rule is that the dependent variables
are in the left term and the indepenent ones in the right term, and they
must not overlap.

The terms get jumbled about, so it IS possible to end up with
a recursive solution, but definitely NOT in this case.

The problem with alpha-conversion is that say the independent
variables are converted, then, when you get the MGU, they
have to be converted back.


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

[John Skaller2]

> On 21 Aug 2018, at 01:45, John Skaller2 <ska...@internode.on.net> wrote:
>
>
>>
>> HOWEVER when I try to make uniq T a subtype of T all hell breaks loose.
>
> Got it!
>
> Felix thinks uniq T = T. The reason is quite obscure: idiot me
> didn’t alpha-convert.
>
> recursion in unification, terms: uniq((<T8682>)) = <T8682>
> Function domain <T8682> = argument type uniq((<T8682>))

So here is the new problem:


proc storeat[T] ( p: &>T, v: T) = { _storeat (p,v); }

The first arg is a write-only pointer. &T is a read/write pointer
which is a subtype of a write only pointer.

I am calling with this argument type:

&uniq((_ustr)) * uniq((_ustr))

Now, it looks like if you set

T <- uniq _ustr

we get

&T * T

Now, the uniifcation should split into two pieces for a tuple,
and we have

&>T >= &T
T >= T

so it should unify: the first inequation says &T is a subtype of &>T.

This worked fine until I ADDED A RULE which says:

T >= uniq T

That is, uniq T is a subtype of T. In other words, a function accepting
a T argument will also accept a uniq T. (In effect, if T is a _ustr, it
is a pointer to a char array, and we can’t modify it because that would
be a side effect. If the function accepts a uniq _ustr instead it can
modify it because it has exclusive ownership).

But see now, what the unification does:


wref(<T5464>) * <T5464> >= &uniq((_ustr)) * uniq((_ustr))
Trying wref(<T5464>) * <T5464> >= &uniq((_ustr)) * uniq((_ustr))

OK so split into two equations:

wref T >= &(uniq _ucstr) //1
T = uniq _ustr //2

Trying <T5464> >= uniq((_ustr)) //2
Trying <T5464> >= _ustr // subtyping rule for uniq ( V >= uniq Q provided V >= Q)


Trying wref(_ustr) >= &uniq((_ustr)) //1
Trying _ustr = uniq((_ustr)) // subtyping rule for wref X >= &X

EQUALITY! We need covariance here!


The problem seems to be that we want

_ustr >= uniq _ustr

but we get equality instead because pointer subtyping conversions are
not covariant.

The idea of the subtyping rule is that

X >= uniq X

for all X, but I didn’t want

T >= uniq X

to lead to the assignment of a variable:

T <— X

So I shouldn’t be adding an inequality T >= X: if X is actually T the rule
applies but it doesn’t actually add new equations, it just passes.

Actually

T >= uniq T

for type variables cannot occur because the dependent variables for
inequalities are always on the LHS, and never on the RHS.

But this begs the true question: if a function accepts an
argument of type T, and you pass a uniq X to it, should it
work?

The answer is yes, but with T set to X, NOT to uniq X.

The thing is, uniq is NOT a functor. Its NOT a proper type constructor.

The problem is like this:

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

MUST FAIL if T is uniq X because it duplicates a uniq value.
But it works otherwise.

We cannot allow this. This is the kind of rubbish C++ does
with const and ref. It changes the semantics so it isn’t
parametric.

What Rust does is correct: a bare T is uniq. If you want a non-uniq
thing you specify non-uniq. [Actually Rust cleverly distinguishes
uniq things from copyable things with type classes .. very clever]

The point is not that I ran into a problem with subtyping uniqs,
the problem is that it is ALREADY inconsistent.

A type variable cannot be set to a uniq thing. The problem worse though:
it cannot be set to a product *containing* a uniq thing (for the same
reason: you can do things to a T you are not allowed to do to a uniq
thing, directly, or indirectly if it is, for example, a componant of a product).

Hmmmm….


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

[John Skaller2]

Here’s a possible solution..

Strip out all “uniq” when unifying. Then, when it comes time to bind
an argument to a paremeter, insert a coercion as usual.

For example:

fun f(x: int) => …
f (box 1) …

We have to add a coercion:

f ( (box 1) :>> int) ..

The coercion here is “unbox”, i.e. we need the coercion to translate to

f ( unbox (box 1) )..

The type of unbox (box 1) is of course just int.
A realistic case:

var x = box 1;
f (x) // OK

There are two issues. First, if the uniq is *nested* the coercsion has to
move “inside”, but coercions already do that.so it should be possible to
make it work. The only trick is if some boxes have to be unboxed and
other don’t. Hmmm … :-) :)

The second issue is that this make it impossible to overload on uniq:

fun f(xint) ..
fun f(x :uniq int) …

If we strip out uniq’s then both

f 1
f (box 1)

will fail with an ambiguity. You won’t be able to have two overloads of
a function with the same name in the same scope one taking a uniq
and the other not.

This makes some sense as follows: if you have a say a char pointer,
or a uniq one, then you may want a function that “upper cases” the string.
It make sense for the uniq version to do it in place, and the non-uniq
version to do a copy and update that. This would become impossible:
you would be required to use two distinct function names.

Hmm…


BTW: I tried this but it failed:

| BTYP_type_var _, BTYP_uniq _ -> raise Not_found
| t1, BTYP_uniq t2 -> add_ge (t1,t2)

The idea was to bomb out if the parameter is a type variable,
so the second match won’t set a type variable to a uniq.
But I have code that uses that:

class Repr[U] { virtual fun repr : U -> string; }

instance[T] Repr[uniq T] {
fun repr(var x:uniq T) => "uniq " + (C_hack::cast[T] x).str;
}

Here we need U to be set to uniq T for some T eg int,
or a char array. Without allowing that, there’s no way
to print the value with “uniq” in front. And THIS function,
namely “repr” cannot be renamed because it is dictated
by the type class.

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

[John Skaller2]

Possible hack: try matching as usual, if that fails and the argument is a uniq type,
unbox it and try again.

This will only work for the argument as a whole, it won’t work for components.

So a second method is that, if we have a product, unbox it t the top
level (if boxed) and then unbox the components (if boxed),
recursivley. This handles arguments like

fun f(x:uniq T, y:U)
var x = 1,”hello”;
f x …

where the top level type is a product that isn’t boxed, but one
of the components is. Its still overkill and doesn’t handle all
possible cases (which unification would if I could get it to work).


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

[John Skaller2]

I would like to announce I am now implementing the next level of the
Felix kinding systems. This is a MAJOR ADVANCE.

As you may know Felix has had a single primitive kind TYPE,
the kind of all types, and two kind constructors: tuples and
functions. Function kinds like:

TYPE -> TYPE

are the kind of type functions like

typedef fun (x:TYPE):TYPE => x * x;

and are required for one case in the library: monads:


class Monad [M: TYPE->TYPE] {
virtual fun ret[a]: a -> M a;
virtual fun bind[a,b]: M a * (a -> M b) -> M b;
fun join[a] (n: M (M a)): M a => bind (n , (fun (x:M a):M a=>x));
}

It took a while to get this to kind check!

Now, here is a real nasty, which DOES NOT WORK PROPERLY:

//$ Join two arrays (functional).
fun join[T, N, M] (x:array[T, N]) (y:array[T, M]):array[T, N + M] = {

var o : array[T, N + M];

if x.len > 0uz
for var i in 0uz upto len(x) - 1uz
call set (&o, i,x.i)
;
i = x.len;
if y.len > 0uz
for var k in 0uz upto len(y) - 1uz
call set(&o,i + k, y.k)
;
return o;
}


The reason it is wrong is two fold. First, N + M is indeed a type,
and indeed it is a suitable type for the result array, it just isn’t
the type you expected because N + M is a SUM TYPE, so
the join of an array index 5 with an array index 7 is an array
with index 5 + 7 and NOT 12 as you might expect. There’s
no way to write a suitable addition.

The second problem is related: whatr if the array incdices are
not unitsums??

What we probably wanted is:

fun join[T, N:UNITSUM, M:UNITSUM]

(x:array[T, N]) (y:array[T, M]):array[T, N \+ M] = {

where \+ is the addition of unitsums. The idea is that UNITSUM
is a SUBKIND of the kind TYPE.

Here’s another nasty:

typematch xx with
| A -> B => 1
| _ -> 0
endmatch

The idea is a predicate that tests if a type if a function type.
This actually works! The problem is, it returns a type,
either 1 (unit) or 0 (void). You may have Ceen (sic) this
Crap (sic) before:

int cond = x > y;

C had no bool, it just use int 0 for false and non-zero for true.

What we actually want is a new kind BOOL here.


Perhaps later, the kinding machinery can be extended to
operate at run time .. and, also, we might get some dependent
typing to work!




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

[John Skaller2]

Here we go! The first working case:


typedef fun _usadd (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("+",(x,y),UNITSUM);

var x : _usadd (5,7) = `1:12;
println$ x._strr;


So, the special operator _typeop takes three arguments:

1. The string name of the operator
2.The type to apply the operator to
3. The kind of the result

The kind of the argument is deduced from the argument.
In this case x and y are specificed as kind UNITSUM.
The argument is kind KND_tuple, a product of kinds,
in this case the kind is written:

UNITSUM * UNITSUM

The result is a UNITSUM. The implementation is in the compiler.
The result of adding type 5 to type 7 is type 12. This is proven by the line:

var x : _usadd (5,7) = `1:12;

type checking. Assuming the compiler type checking is correct.

The print is there so we can see the result:

case 1 of 12

aka `1:12. So the model is to write the type functions as wrappers around the primitives,
so we can then more easily combine them, for example:

_usadd (1, _usadd (2,3))

would be type 6. The implemetation of + is done, to follow are many more
operations such as:

- (difference)
* (multiply)
/ (divide)
% (remainder/modulus)


There is much more to be done. For example comparisons:

< > <= >= == !=

but these should return TRUE or FALSE which are of kind BOOL
and NOT a type. Lots of existing bad code needs fixing now.
For example I have to add a kind:

TYPESET

and an operator

_in_typeset: TYPE * TYPESET -> BOOL

This is an example of a constraint. Felix polymorphic argument lists can have
constraints, but the syntax is hacked, and the evaluation returns 0 or 1,
which are types, instead of FALSE or TRUE.

Also I have to think whether to use

`+
`*

for unitsum addition and multiplication since I can’t use + and * as they’re taken
as type constructors for sum and product types, respectively. Not sure I want to
fix that syntax just yet, it uses up a valuable symbol.

BTW this works too:

var x : ( 5 `(_usadd) 7 ) = `1:12;



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

[John Skaller2]

[John Skaller2]

So this now WORKS:

////////////////
var x : (5 `+ 7) = `1:12;
println$ x._strr;

//$ Join two arrays (functional2).
fun xjoin[T, N:UNITSUM, M:UNITSUM] (x:array[T, N]) (y:array[T, M]):array[T, N `+ M] = {

var o : array[T, N `+ M];

if x.len > 0uz
for var i in 0uz upto len(x) - 1uz
call set (&o, i,x.i)
;
i = x.len;
if y.len > 0uz
for var k in 0uz upto len(y) - 1uz
call set(&o,i + k, y.k)
;
return o;
}

var a = 1,2,3,4;
var b = 5,6,7,8;
var c : int ^ 8 = xjoin a b;
println$ c;
//////////////////////////////

I have provided new operators:

`+, `-, `*, `/, `%, `max, `min, `gcd, `lcm

which can be applied to unitsums. The important use is shown here:

fun xjoin[T, N:UNITSUM, M:UNITSUM] (x:array[T, N]) (y:array[T, M]):array[T, N `+ M] = {

This routine joins two linear arrays. by linea I mean the arrays are indexed by unitsums.
This routine was incorrect before because it returned and array indexed by type

N + M

which is not a linear array. In case you’re wondering here’s an example of that:

(1,2,3),(4,5)

That is an array! But it is not a linear array, it has type

int ^ (3 + 2)

Yes, that really works. Its a legit type, and the old routine have a legit result,
and the result was layout compatible with a linear array. For example

join (1,2,3) (4,5) == (1,2,3), (4,5)

but that isn’t what we wanted, we wanted

1,2,3,4,5

There is no way to do that without being able to add 3 to 2 and get 5.
Now we can do that:

3 `+ 2 = 5

Using the unitsum addition operator `+. The problem is that `+ only works on
unitsums, so you cannot just add two type variables unless you KNOW they’re
unitsums and there was no way to say that.

Now there is, as you can see:

N:UNITSUM

says the type variable N has kind UNITSUM so the addition is safe.

The work is NOT complete, I’m not sure the constraints are properly checked
or that overload resolution works on kinds. In fact I’m pretty sure it doesn’t.
What I mean is that if you have two type functions with the same name like:

typedef fun pair (X:UNITSUM, Y:UNITSUM):TYPE => X `+ Y;
typedef fun pair (X:TYPE, Y:TYPE):TYPE => X * Y;

then

pair int long // should call the second function
pair 2 3 // should call the first function

in this case, we’re overloading on two kinds, one of which happens
to be a specialisation of the first. I dunno if this works but I suspect not.
For the moment JUST DONT if it is possible to avoid this.

There is much more to be done. There are now cases where previously
we assumed we could calculate the size of a unitsum but now we have to
defer the calculation until type variables are removed and the addition
is reduced away.

Note that the polymorphic type system is now, effectively, dependently typed.
However since Felix has no run time polymorphic entities, monomorphisation
resolves the calculations. In other words the X `+ Y will reduce to a unitsum
with a size known at compile time. Therefore things like:

zip: T ^ N -> T ^ M -> T ^ N

which combines two arrays of the same length into an array of pairs,
can be type checked by verifying the length of M = N after monomorphisation.
What we need here is to WRITE the constraint and propagate it so
the check is actually done, i.e. we want to add the constraint:

N `== M

to the type of zip. This is dependent typing. Dependent typing is hard to do
but in Felix the “type known only at run time” is reduced to “type known
only after monomorphisation” so we do not need the complex proof generation
machinery real dependent typing systems require, our proofs can all be
generated by simply evalation the type expressions after monomorphisation.

At present `== isn’t defined, I have ONLY implement these:

ypedef fun n"`+" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("+",(x,y),UNITSUM);
typedef fun n"`-" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("-",(x,y),UNITSUM);
typedef fun n"`*" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("*",(x,y),UNITSUM);
typedef fun n"`/" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("/",(x,y),UNITSUM);
typedef fun n"`%" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("%",(x,y),UNITSUM);
typedef fun n"`min" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("min",(x,y),UNITSUM);
typedef fun n"`max" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("max",(x,y),UNITSUM);
typedef fun n"`gcd" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("gcd",(x,y),UNITSUM);
typedef fun n”`lcd” (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop (“lcd",(x,y),UNITSUM);

I need to handle BOOL, this is the kind of constraints, so for example:

typedef fun n”`==” (x:UNITSUM,y:UNITSUM):BOOL=> _typeop (“==,(x,y),BOOL);

but that requires implementing the _typeop. In turn I have to add BOOL_true
and BOOL_false as type terms (but they are not types!).

In normal code, x can be type “int” or maybe type “bool”.
WIth types, x can be kind TYPE or kind BOOL.

The “type term” x doesn’t have to be a type, more precisely, the notion of
“type” is actually just a compile time constant or type constructor of any
kind at all. We just have to kind it as we type ordinary expressions.

I am not looking forward to the logical extension .. kind classes.
Like type classes .. only one level up :-)

And if we have kinds .. well we will need SORTS as well to “type” them.
ARGGGGG.


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

[John Skaller2]

So .. I have added kind BOOL with two values `true and `false, and operations
`and, `or, `xor, `not. I aldo added `< `> `== to UNITSUM, which was the goal,
but required BOOL for the result. The kind BOOL is called staticbool because its
a compile time bool.

The idea is to form a constraint. Not test yet.

Unfortunately there is an issue: x `< y for unitsums is not a specialisation of x `< y for types,
meaning x is a subtype of y, because unitsums don’t subtype because sums dont.
In principle, they do, in Felix they don’t. Polymorphic variants do thoughl The choice
was deliberate. Hmm.

But there’s worse to come! Consider

`if c `then t `else f `endif

I can define that for unitsums. And for types. And for staticbools.
And for ANY kind!

So we need overloading but better ,,, POLYMORPHISM. Over ***kinds***.
Which means I need kind variables.

typedef fun ifthenelse[K:KIND] (c:BOOL,t:K,f:K) => …

And what is that word “KIND”? Its a SORT!!!!!!

======

There’s also another problem. Ocaml. Its a weak language!
TO define < on types to mean subtyping I have to call unification.
But I can’t because it isn’t defined yet.

But I can’t move the kinding ops ahead of it, because they call the
BTYP_typeop constructor, which is private to the file defining it.

Now, I can define a wrapper, which is private, and pass it forward.
But then the problem is, how does the constructor call forward without
passing the kinding ops functions backwards????

Its not impossible by the problem is you can only pass *functions* as
parameters, but the kinding ops code also does pattern matching.

Felix is just a much better language!


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

[John Skaller2]

Executive summary: I’m looking at removing RE2 from Felix and using C++ standard library regex instead.

Examining Felix regex support, we primarily use a DSSL to make regular definitions,
we do NOT like regex much, regdefs are much better.

What Felix does is take a regular definition and *render* it into a regex string which is then
compilerd by the underlying regex engine (RE2 at the moment) into a regex matching
object which can then be used to perform a match. Note at present Felix does NOT
support searching, only whole string matching, because there is no logical need for
searching, just match “.*regex.*” to do a search. Also there is no “shortest match”
support which IS actually required (I have needed it many times!).

Felix does support matching on a substring represented by an RE2 specific
thing called a StringPiece. You need this if you are, say, tokenising a string,
to avoid copying the match tail so you’re ready to find the next token:
StringPiece is a *view* of a string. C++17 (I t hink, maybe 20?)
has a string view class that can do this.


Felix identifies submatch results by number. There’s no support for named submatches,
that would be nice but isn’t available.

Felix uses an RE2 specific mechanism to query the result object.

RE2 provides a NumberOfMatchingGroups method, which is required to allocate
a Felix varray of submatches from a result. Standard C++ regex provides mark_count
method which does the same thing.

I checked the rendering engine and it should work for both,
Render translates repetition counts to * + ? which should work
for both libraries just fine.

Strings are translated as follows: alphanumerics are emitted as written,
all other chars are converted to \xFF format. ECMA script supports this.
RE2 uses () for capturing groups and (?: … ) for non-capturing groups.
ECMA script is the same.

So it looks doable for the matching except for the string piece interface.
Standard C++ is using iterators here.

It looks doable if I can change the way views of strings work.


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

[John Skaller2]

Ah, I think i have a solution to the uniq issue.

The problem is that we want a uniq T argument to work with a function
with a plain T parameter. Its safe to “throw away” uniq: we own the value,
we can do what we like with it. So the original idea was to make
uniq T a subtype of T. But this broke:

proc storeat[T] ( p: &>T, v: T) = { _storeat (p,v); }

Whilst a write only pointer to T, &>T is a subtype of a general
pointer &T which can read and write, the T is invariant.

Now, I want to pass a uniq T for v and have it degrade by subtyping
to a plain T. But this requires the T in the type of p to degrade as well,
but there’s no subtyping of the pointed to type, not even for uniqs.
(The pointer &T degrades by subtyping to &>T but not the T).

The solution is a hack! Allow just this one subtyping conversion!
In other words allow

&T ===> &>T

AND

&(uniq T) ===> &>T

but no other subtyping. Ditto for read-only. Normally we can’t easily allow pointer
subtyping even though it is algebraically sound because its really hard to implement
for machine pointers. It is allowed for abstract pointers (I mean, it actually works
for them because the rules for the get and set methods of an abstract pointer
subtype automatically).

The rule is a bit of a hack because it doesn’t propagate to products.
But then I’m not sure it should.

The case we do NOT want to allow is passing the address of a non-unique pointer
to a function with a pointer to a uniq parameter. That function can legitimately believe
it owns the store pointed at exclusively and write to it, so if we allowed the subtyping
in this case we the function would break the callers expectations that the function
knew the pointed at store could be shared.

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

[John Skaller2]

> On 3 Sep 2018, at 12:34, John Skaller2 <ska...@internode.on.net> wrote:
>
>
> Ah, I think i have a solution to the uniq issue.

Well the unification engine now says this:

| BTYP_wref t1, BTYP_wref (BTYP_uniq t2)
| BTYP_wref t1, BTYP_pointer (BTYP_uniq t2)
(*
| BTYP_rref t1, BTYP_rref (BTYP_uniq t2)
| BTYP_rref t1, BTYP_pointer (BTYP_uniq t2)
*)
-> add_eq (t1,t2)

| t1, BTYP_uniq t2 -> add_ge (t1,t2)

The LHS is the function parameter type, the RHS is the argument type.
Add_eq specifies invariance, whereas add_ge allow subtyping.
The code above is part of the subtyping rules.

This change allows pass-by-vale to “throw away” uniq.
However overloading still works:

////////////
proc show (var x:uniq int) {
println$ "Uniq " + x.str;
}
proc show (var x:int) {
println$ "NON Uniq " + x.str;
}

begin
var x = box 42;
show x;
end
//////////

This code will print Uniq 42. If the first procedure
is deleted it prints NON Uniq 42. So you can pass a uniq argument
to a non-uniq parameter, but if there is an overload with a uniq
parameter it is preferred.

The pointer subtyping rule is weird. It allows you to store a uniq value
at a location specified by a pointer to a non-unique store.
in particular this routine:

proc storeat[T] ( p: &>T, v: T) = { _storeat (p,v); }

will work if v is uniq, but p points to a non-unique.

//////////
proc show (var x:uniq int) {
println$ "Uniq " + x.str;
}
proc show (var x:int) {
println$ "NON Uniq " + x.str;
}

begin
var x = box 42;
var y : int;
storeat (&y, x); // <—- &y nonuniq, x uniq
show y;
var z : uniq int;
storeat (&z, 42); // <—— &z uniq, arg non-uniq
show z;
end
/////////////

The rule ensures the uniq of x above is “thrown away” in
the call. Without the special pointer rules, invariant subtyping
of pointer targets prevents the uniq being thrown out
“under the pointer”.

It also allows a non-uniq value to be assigned to a uniq store.

Note the unification rule I commented out the equivalent handling
of read-only pointer because that breaks code. I don’t really
understand why :)

I’m not sure I fully understand if the subtyping rules in the
unification are sound.


GENERAL COMMENT
—————————-

When a function returns a “first class value” it is intrinsically unique.
Its an rvalue, or, if you like, stored in a temporary. The function which
accepts that value is the only user, and is free to write to it, because
the temporary isn’t sharable because it is unknown except to the
function accepting it. In other words you can write to a parameter
because its a copy of the argument if the argument were a variable
and it is the temporary otherwise. You can say the value is MOVED
from the temporary to the parameter instead.


So the whole of the problem is with variables, which have to be
copied instead of moved in general because they variable shouldn’t
change just because it is passed to a function as an argument.
So IN PRINCIPLE uniq has nothing to do with values, only with variables.
So using a TYPE COMBINATOR is just wrong.

In fact, a variable is REALLY a pointer. It points at the store.
When you use the variable name in an r-context, it is dereferenced
automatically, or more precisely the value fetched, in an l-context
it is the address of the store so you can assign to it.

So really uniq is a POINTER QUALIFIER.

In particular those temporaries aren’t uniq, but the pointer the temporary
actually is, THAT is uniq. And when passed to a parameter we can do
a move because of that.

So the fundamentals are that there are NO VALUES only pointers.

copy (&T, &T) // LH is target, RH is source
move (&T,&T) // ditto

are the fundamental non-uniq ideas, so this is actually:

cp (&>T, &<T)
cp (&>T, &uniq< T) // move!

In other words, if the poiter to the store to be copied is uniq,
we do a move instead .. using an OVERLOAD. This should
cause the source of the move to become inaccessible.
Its hard if not impossible to implement this because of pointer
aliasing.


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

[John Skaller2]

And here is the low hanging fruit!

I want to make this work:


var x = ..[5];
for i in x perform println$ i._strr;

The notation ..[5] is a slice through ALL the values of a given type.
So ..[tiny] ranges through -128..127. And ..[5] should range through
`0:5, `1:5, `2:5,`3:5,`4:5.

Now, 5 is a unitsum, and slice iterators at the moment require a value
of Integer class. That’s no good, Integers are too powerful. So I defined
these instead:

///////////////////////////////////////////
// Forward iterable
class Forward[t] {
virtual fun succ: t -> t;
virtual proc pre_incr: &t;
virtual proc post_incr: &t;
}

// Totally ordered forward iterable
class TordForward[t] {
inherit Forward[t];
inherit Tord[t];
}

// Bounded totally ordered forward iterable
class BoundedTordForward[t] {
inherit TordForward[t];
virtual fun maxval: 1 -> t = "::std::numeric_limits<?1>::max()";
}

// Bidirectional
class Bidirectional[t] {
inherit Forward[t];
virtual fun pred: t -> t;
virtual proc pre_decr: &t;
virtual proc post_decr: &t;
}

// Totally ordered bidirectional
class TordBidirectional[t] {
inherit Bidirectional[t];
inherit Tord[t];
}

// Bounded totally ordered bidirectional
class BoundedTordBidirectional[t] {
inherit TordBidirectional[t];
inherit BoundedTordForward[t];
virtual fun minval: 1 -> t = "::std::numeric_limits<?1>::min()";
}

// Bounded Random access totally ordered
class BoundedTordRandom[t] {
inherit BoundedTordBidirectional[t];
virtual fun + : t * t -> t = "$1+$2";
virtual fun - : t * t -> t = "$1-$2";
virtual fun one : 1 -> t;
virtual fun zero : 1 -> t;
}
///////////////////////////////////////

and changed the iterators to be like this:

///////////////////////////////////
gen slice_from_counted[T with BoundedTordRandom[T]] (first:T) (count:T) () = {
var k = count;
while k > #zero[T] do
yield Some (first + (count - k));
k = k - #one[T];
done
return None[T];
}
/////////////////////////////

Now I need this .. and here is where MAGIC comes in:

///////////////////////////
instance[T:UNITSUM] Eq[T] {
fun == (x:T,y:T) => caseno x ==caseno y;
}
instance[T:UNITSUM] Tord[T] {
fun < (x:T,y:T) => caseno x < caseno y;
}
instance[T:UNITSUM] BoundedTordForward[T] {
fun maxval () => (memcount[T].int - 1) :>> T;
}

instance[T:UNITSUM] BoundedTordBidirectional[T] {
fun minval () => 0 :>> T;
}

instance[T:UNITSUM] BoundedTordRandom[T] {
fun + (x:T,y:T) => (caseno x + caseno y) :>> T;
fun - (x:T,y:T) => (caseno x - caseno y) :>> T;
fun one () => `1:T;
fun zero () => `0:T;
}
///////////////////////////

Notice the subkinding constraint on the instance type variable!!!!
Most of the operations would be nonsense on other types.

And lo .. it works. Although all the other iterators are broken now
because integers are not sequences yet.


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

[John Skaller2]

I have finally eliminated interscript totally. It only took, what, 10 years?

Felix no longer needs or uses fbuild generated configuration information,
except for 3 values:

* the platform: osx, posix, linux, windows
* the compiler word size (32 or 64 bits)
* the compiler (clang, gcc, or msvc)

All the configuration data is in the config database, and the above 3 variables
are used to establish the config database contents (fpc files), host dependent
C++ header files, and Felix macro file. This is a prelude to a Felix configuration
program that can set up a new target. Currently you have to copy an old
target configuration (usually “host”) and hand edit it.

instead of determining a whole host of paremeters, the system now
comes with prebuilt configurations for

macosx, linux, windows
clang, gcc, msvc

Windows ONLY runs 64 bits. I personally want to run BOTH clang and gcc on
my Macbook pro, if only to see which is faster (it will probably be gcc because
clang’s people refuse to allow assembler labels, which are needed to use
computed gotos for resumptions, which are probably faster than the C switches
used for clang).

There are also now config database entries (fpc files!) for

cplusplus_11
cplusplus_14
cplusplus_17
cplusplus_20

the last one being a bit hopeful. You can do this:

//////////
type cxx = "int" requires package "cplusplus_17";
ctor cxx: int = "$1";
ctor int: cxx = "$1";
instance Str[cxx] {
fun str (x:cxx) => x.int.str;
}

var x = cxx 42;
println$ x;
/////////

The requires package requires a header file which checks __cplusplus
macro and #error’s out if the compiler isn’t capable of handling it.

It also sets the appropriate switch on the compiler command line.
This doesn’t work right yet because if you mix C++11 and C++14, say,
you just get BOTH switches instead of “the greatest”. Its not clear
if you can actually mix object files compiled for different language versions.
So if you do several C++ compiles as well as a Felix compile it could be messy.
Not sure. In any case I have to figure out how to get “the greatest” switch.

I’m going to make the toolchains more parametric, that is, read things
like the compiler executable name from a file. At present, g++ comes
in Debian packages with names like g++-5, g++-6, etc which avoids
clobbering your system compiler .. but Felix toolchains demand just “gcc”
which means you’d need to compiler a plugin for each possible
version.

I also want to add Copyright licence controls to the system.
The idea is simply to include a “copyright: Authorname” field or fields
to library *.fpcs, and also a “licence: GPL” field. This could allow
finding the list of all contributors to your program, and, also,
listing all the applicable licences. Later some controls might be added
to bomb a build that exceeds your licencing policy.



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

[John Skaller2]

So, I have no managed to get

flx —target=gcc_macosx hello.flx

to work on my box. The host system uses clang. GNUmakefile contains gcc_macosx target
to build it:

gcc_macosx:
# =========================================================
# prepare for gcc build on macosx
# =========================================================
flx_build_prep --target-dir=build/release --target-bin=gcc_macosx --source-dir=build/release \
--source-bin=host --clean-target-bin-dir --copy-compiler \
--configure --compiler=gcc --os=macosx --bits=64 --debug

# =========================================================
# build gcc rtl on macosx
# =========================================================
${LPATH}=build/release/host/lib/rtl flx_build_rtl --target-dir=build/release --target-bin=gcc_macosx

# =========================================================
# build Felix with gcc rtl on macosx
# =========================================================
${LPATH}=build/release/host/lib/rtl flx_build_boot --target-dir=build/release --target-bin=gcc_macosx --build-all


Note the NEW options for build_prep: —configure says to build a new configuration.
—compiler specifies the compiler, —os the operating system, and —bits the word size.

The configuration is generated by COPYING FROM THE CONFIG DIRECTORY.
The ONLY thing generated is the toolchain.fpc file.

The fbuild boostrap does the same copying. Interscript is gone.
Generated files are gone (except the toolchain.fpc file).

Three compilers are supported:

* gcc, clang, msvc

Three OS are supported:

* linux, macosx, win

Two bit sizes are supported:

32, 64

except on win, where only 64 bits are supported. Stuff have been renamed to make
the combinations fully parametrically regular. Pre-build configuration data is in
the repository. fbuild dtects the correct OS and sets gcc for iinux and clang
for macosx.

Other OS could be supported but aren’t, and probably won’t be unless someone
asks. Eg generic Unix or BSD, Cygwin, MSYS, iOS, Android etc.

However now I am analysing the structure of the system I want to change the layout a bit, again.
First, make it work .. then break it :)

* The first problem is that when using multiple targets the cache is trashed when
you switch targets. Rather I should say .. I HOPE it is trashed because we don’t
want to mix clang and gcc binaries in the cache, because with C++ they’re
incompatible. The text cache will usually be the same, but Felix does support
conditional compilation.

* The second problem is that I hate that the targets and the share directory
are mixed up in the same directory (the Felix version install directory by default).

* The third problem is that the build in the GNUmakefile creates a new host.
To be specific it creates a unified host and target. This means it builds
flx and other tools. My setup does NOT build the compiler but copies it.

IN PRINICPLE this is wrong. A target should ONLY consist of header files,
object files and binary libraries, and config database. ONLY a host
needs the compiler and tools like flx. If you are cross compiling on Linux
for Windows, you should be able to build a program but not run it,
and obviously a “flx” built for Windows won’t run on linux.

So IN PRINCIPLE the host and target should be split:

/usr/local/lib/felix/felix-version/
share
hosts
targets

With this layout, the system can live on a shared server drive
which can be accessed and used from say Linux AND Windows.

In fact, on such a system, Windows compilation on Linux could
be done with remote procedure calls or something similar.

* The cache obviously has to be partitioned as well.
We need at least to split the cache/binary directory up by targets.

The sources to compiler are generated by the host so cache/text
has to be split by hosts.

IN ADDITION for commercial server application, the cache needs to
be divided by process or at least protected by locks. I propose
that this is a “pay for it” option. Free users can create multiple
accounts OR specify distinct caches for each process manually
(you can do that, in fact the build system puts the cache
in build/cache to avoid clobbering the cache in your account).

SO as a user to use two distinct hosts you would just create two
terminals. If you use the same host concurrently, it will usually
work (if two processes write the same file simultaneously it doesn’t
matter because they usually write the same thing). There’s only
a problem if something differs such as the Felix version,
Felix library or grammar.

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

[John Skaller2]

I am adding two optional fields to the toolchain.fpc config, for example:

toolchain: toolchain_gcc_linux
c_compiler_executable: gcc-8
cxx_compiler_executable: g++-8

The extra fields specify the pathname of the compiler executable.
If omitted, Felix uses the defaults:

gcc,g++
clang,clang++
cl

There’s a pain without this, because the toolchains currently *mandate* the compiler
executable name, which means if you have say, and old MacOS or Linux distro,
and you add newer versions of the compilers, the package managers such as apt,
brew, etc, install the new compilers with specific version names, specifically
to PREVENT confusion with the OS vendor supplied compilers.

We often want to use a modern compiler .. to get C++14, C++17 and C++20
features.

So, the big hassle is now getting those fields set. Of course you can just go and edit them,
but the next rebuild of Felix will clobber your edits.

The fbuild bootstrap needs to set thses .. but I don’t know how to get the
information from fbuild …

After that I don’t know how to preserve the fields. Possibly, the fields should go
in a distinct *.fpc file so they can be copied from the ~/.felix/config directory,
which is the source of persistent mods when rebuilding Felix.



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

[Ryan Gonzalez]

When you get a builder, e.g.:

c_builder = fbuild.builders.c.guess_shared(...)

You ca get the executable via c_builder.compiler.exe. 

To figure out the type of compiler (e.g. Clang vs GCC vs MSVC) you can do:

if isinstance(c_builder, fbuild.builders.clang.Builder):

    # Clang

elif isinstance(c_builder, fbuild.builders.Gcc.Builder):
    # GCC

elif isinstance(c_builder, fbuild.builders.msvc.Builder):

    # MSVC

Note that Clang has to be checked first because of the inheritance hierarchy. 

--
You received this message because you are subscribed to the Google Groups "Felix Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to felix-languag...@googlegroups.com.
To post to this group, send email to felix-l...@googlegroups.com.
Visit this group at https://groups.google.com/group/felix-language.
For more options, visit https://groups.google.com/d/optout.

--

Ryan (ライアン)
Yoko Shimomura, ryo (supercell/EGOIST), Hiroyuki Sawano >> everyone else
https://refi64.com/

[John Skaller2]

> On 20 Sep 2018, at 15:16, Ryan Gonzalez <rym...@gmail.com> wrote:
>
> When you get a builder, e.g.:
>
> c_builder = fbuild.builders.c.guess_shared(...)
>
> You ca get the executable via c_builder.compiler.exe.
>
> To figure out the type of compiler (e.g. Clang vs GCC vs MSVC) you can do:
>
> if isinstance(c_builder, fbuild.builders.clang.Builder):
> # Clang
> elif isinstance(c_builder, fbuild.builders.Gcc.Builder):
> # GCC
> elif isinstance(c_builder, fbuild.builders.msvc.Builder):
> # MSVC
>
> Note that Clang has to be checked first because of the inheritance hierarchy.

Ah, ok thanks!


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

[John Skaller2]

I have to apologise that most of the builds are failing.

1. Appveyor/Windows builds have started to fail for an unknown reason.

It worked fine, but now crashes with a bug creating a process under Windows
in the fbuild Python scripts. I have no idea how to fix it.

In general Python development is crap. I advise DO NOT USE PYTHON.
Every version introduces breaking changes.

2. Linux build fails because Ocaml team also introduced breaking changes.
Ocaml is crap. DO NOT USE OCAML.

First they stupidly changed strings to be immutable due to their own
idiotic design fault, and introduced bytes, which are mutable.
Mutable strings still work, but they’re not going to be supported for ever.
Painfully I upgraded everything except the Dypgen executable which I couldn’t
figure out how to fix. Dypgen is no longer maintained. The build still works
by allowing that one tool to be built with -unsafe-string.

Worse, new API’s are required to translate strings/bytes and their
only available in Ocaml 4.06.1 and above. In addition the idiots
removed BigNum package which Felix was using so I had to remove
dependence of that as well. This required cutting down the OCS Scheme
library which also used it. OCS isn’t maintained either.
The morons replaced it with a binding to gmp, but gmp isn’t available on Windows.
So now we no longer have R5RS scheme in the parser, but only a subset of it.

Ocaml is also very hard to build correctly on Windows.
There is a binary on GitHub however.

3. So on Linux .. you have to build Ocaml from source
because the moronic Debian system thinks distributions
have fixed packages in them. Older versions of Debian
or Ubuntu suich as Travis runs cannot install Ocaml 4.06.
SO you have to build it from source and clobber your apt-get
installed Ocaml.

4. Felix is upgrading to higher levels of C++ Standard.
Because of this you need a recent C++ compiler.
Again, stupid Ubuntu wont let you download new packages.
You have to add a line to /etc/apt/source or whatever to get experimental
toolchains, then you can apt-get install g++-8.

Unfortunately it doesn’t name the compiler g++. Stupid crap again.
Felix now lets you specify the compiler executable.

In summary a bunch of idiots have conspired to break their own
software and lay the burden onto clients. Thankfully Felix has
few dependencies but even those are causing problems.

We need to get rid of both Python and Ocaml.

5. I’m looking at replacing the build machinery on Windows
with using Windows 10 WSL: WIndows Subsystem for Linux,
aka Bash for windows. Felix builds on that and it should be
possible to invoke Visual C++ from the Linux built Felix on Windows,
and build an msvc_win target.

I haven’t tried it yet. It would involve starting a console with Visual Studio
environment set up for cl.exe to work correctly, and then starting
a Linux terminal inside that which inherits the environment so that
we can call cl.exe from Linux. In that case the Linux built Felix
can actually be used to build software with cl.exe .. including
rebuilding itself. This way we avoid Python on Windows.

Provided we’re inside the Linux environment, we can use the
Linux build flxg compiler and so don’t need Ocaml on Windows either,
However we would need it to finally escape the doubled up environment,
although .. cmd.exe is a pain for a shell and using Bash is probably
a good way to go. The only trick is that Windows programs cannot
see into the Unix file system. At least the cache defaults to $HOME which
in the doubled up environment is in the Unix filesystem.

It’s likely to be messy. Luckily there are no users.

In the longer term, I would like to get rid of Ocaml by rewriting
the compiler in Felix. Unfortunately whilst most of it is just tedious,
the parser Dygen is going to be really hard. I have no idea how
it works. There is nothing remotely as capable out there.
Dypgen is GLR, scannerless, and extensible. Bison just doesn’t cut it.


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

[John Skaller2]

There is now a subarray function designed so constant slices of arrays (of any size)
can be made to work (they don’t yet). Here’s the function:

fun subarray[FIRST:UNITSUM,LEN:UNITSUM,T,N:UNITSUM] (a:T^N)= {
typedef K =_typeop("_unitsum_min",(LEN, N `- FIRST),UNITSUM);
var o : T ^ K;
for i in ..[K] do
var first = Typing::arrayindexcount[FIRST].int;
var outix = caseno i;
var inpix = (first + outix) :>> N; // checked at run time?
&o.i <- a.inpix;
done
return o;
}

var a = 1,2,3,4,5,6,7,8;
var b = subarray[2,5] (a);
println$ b;
var c = subarray[2,10] a;
println$ c;

The code works but is not what I tried to write!

We give the types FIRST, and LEN, which must be UNITSUM kind,
to specify the first element of the subarray, and, its length. The underlying
array is type T^N, where N is also UNITSUM kind. Arrays with index of
kind UNITSUM and *linear* arrays. So this function won’t work for arbitrary
compact linear types.

With slices, its legal to run off the end, So we have to calculate the
length of the subarray by min(LEN, N - FIRST). Unfortunately, that doesn’t
work as written. The - has to be replaced by `- for symmetry with addition
which has to use `+ because + means to form a sum, not to add the types
numerically. Felix gets confused if I write min, it tries overloading and
comes up with run time min functions, instead of the type function.
So I had to spell out the type function ;(

The real problem is that I can’t specify the return type because K
is defined inside the function. I tried to do this:

fun subarray[FIRST:UNITSUM, LEN:UNITSUM, T,N:UNITSUM,
K=_typeop(“_unitsum_min”,(LEN, N `- FIRST),UNITSUM)]
(a:T^N) : T ^ K = ….


with K inside the type variable binder list. That “should” work but didn’t.

Felix is designed to allow equational constraints. The problem is it means:

[FIRST:…. T,N:UNITSUM,K with K=_typeop( … ]

where the K = _typeop … is a constraint that the LHS and RHS must unify.
In the process of unification, bound type variables have their bindings checked,
and unbound ones are bound. In this case K is unbound, so unification SHOULD
have set K but it didn’t work.

The problem is another special feature. You can write:

fun g(x:ints) => …
fun f (x:uints) => g (x);

where “ints” is a typeset consisting of all the integer types and
uints a typeset of all the unsigned integer types.

Felix checks that the constraint on x in f *implies* the constraint on x
in g, that is, it checks “all uints are ints”.

In Felix typeset is an object like:

typedef ints = typesetof (int,short,long);

which admits a membership test like

int in ints // true!

The membership test is implemented with a type match:

typematch int with
| int => 1
| short => 1
| long => 1
| _ -> 0
endmatch

where 1,0 are unit and void types respectively and are used for true
and false, respectively .. its the same rubbish hack used by C for
booleans before C had booleans. in Felix this design fault will soon
be replaced by TRUE and FALSE of kind BOOL, a compile time
boolean (but this is not done yet, its work in progress).

So .. what *constraint implication checking* does is take two typesets,
expanded into type matches and check that the LHS pattern of every case,
one by one, matches some pattern of the RHS. If every pattern matches,
then, any type which satisfies the first type match must also satisfy the second,
in other words, the first typeset is a subset of the second one, in other
words (again) the first typeset, considered as a constraint on a type,
*implies* the second one.

Constraint implication checking is essential, otherwise, the call to g(x)
inside f must be bombed out because the constraint that the argument
to g is an integer must be failed with an arbitrary type variable. In particular
the short hand is expanded to

fun g[T with T in ints] (x:T) => …

which is expanded to

fun g[T with typematch T with | int => 1 | short => 1 | long => 1 | _ => 0 endmatch] (x:T) …


The PROBLEM is that constraint implication in Felix at the moment ONLY works for
typeset constraints.

It doesn’t work for equational constraints. In fact, this doesn’t matter!
The purpose of the equation constraints is two fold:

* first, it can bomb out a call where the equations aren’t satisfied.
In this case, propagation of the constraint to an inner call by implication
works just fine with no additional code. If the outer constraint fails,
the inner constraint is irrelevant which satisfies implication.

* second, if the outer constraint succeeds, then the inner one may succeed or fail,
but it is just another equation on the outer type variables: it either
unifies or doesn’t. The constraint is *propagated* by substittution.

For example if you have

fun g[U,V with P (U,V)]

where P is some constraint then if you have

fun f[A,B] with Q[A,B] ( … ) => g[A * B, A + B] …

then the inner constraint checked is

P (A * B, A + B)

in other words the constraint of g *specialised* by replacing
the constraints parameters U,V with the arguments A * B, A + B.

“We don’t need no type set implication here”.

Actually we can view all constraints as typesets, which happens
to be one element type sets. Unfortunately Felix is NOT doing that,
it bombs out equational constraints because they’re not explicitly
typeset constraints.

This problem has to be fixed .. eventually. I’m not sure what typesets are.

From one point of view a typeset is a noun which is just a convenience for
specifying a predicate: a set is just sugar making it easy to construct
membership predicates. That is

x in {a,b,c}

is just shorthand for

x == a or x == b or x == c

Sets dont exist, only logic exists, sets are just a sugar to make logic easier
to write.

HOWEVER .. at present typesets constraints just say “yes” or “no”.
The type is in the set or not.

Equational constraints do more than say yes or no. They can also
SET the value of a variable.

And that is indeed the intent for K. In this form:

[FIRST:…. T,N:UNITSUM,K with K=_typeop( … ]

I am not trying to add a constraint on K at all, I’m trying to DEFINE K
in terms of the other type variables.

This COULD be written as a typeset, provided we allow polymorphic elements
in typesets.

In some sense a type set is a (non-discriminated) union type.

That’s my confusion at the moment. In one sense, a typeset is a
subkind of a constraint kind, more precisely a noun kind, which can
be used to construct function returning BOOL, i.e. constraint predicates.

In another sense, it is an actual type constructor. You can look it up
in Wikipedia. They’re a bit arcane but union and intersection types
exist with the “obvious” meaning: a union or two types A and B is just
a type which is in A or in B, an intersection is just a type in both.

I have to decide on which model to use. Anyhow that’s the status:
the hackery in subarray function is enough to implement constant slices
of BIG arrays. (Small slices are implemented like tuples, by listing
the elements inside the compiler .. not a good idea for arrays
of 100,000 elements .. :)


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

[John Skaller2]

however this works:

fun f[T,U=T * T] (x:T): U => x,x;
println$ f 1;

In fact this works too:

println$ f[int, int *int] 1;

and this correctly fails:

println$ f[int, int * long] 1;

Interestingly the error message is:

_typeop(_type_to_staticbool,(typematch int * long with
| int^2 => unit
endmatch),BOOL)
Reduced to _typeop(_type_to_staticbool,(typematch int * long with
| int^2 => unit
endmatch),BOOL)

So you can see, there’s actually a type match in there. The failure is
because it doesn’t reduce .. it should reduce actually .. hmmm.. to
an empty match.

The problem with the subarray case is probably the inability to reduce
the expression… hmm ..


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

[John Skaller2]

> On 27 Sep 2018, at 06:02, John Skaller2 <ska...@internode.on.net> wrote:
>
> however this works:

OMG .. after hours of debugging and test cases I found the problem.
The compiler works fine!

Here’s the solution:

fun subarray[
FIRST:UNITSUM,
LEN:UNITSUM,
T,
N:UNITSUM,

K:UNITSUM=_typeop("_unitsum_min",(LEN, N `- FIRST),UNITSUM)

]
(a:T^N) : T ^ K
=

{

var o : T ^ K;
for i in ..[K] do
var first = Typing::arrayindexcount[FIRST].int;
var outix = caseno i;
var inpix = (first + outix) :>> N; // checked at run time?
&o.i <- a.inpix;
done
return o;
}

You need to look hard to see the fix!

The problem was that K was given kind TYPE.
In the code above .. which surprisingly works .. I mean it actually parses ..
I just set the kind to UNITSUM and lo .. it just works.

The *default* kind of a type variable is TYPE. The kind isn’t deduced
from the kind of the RHS of an assignment such as for K above,
although perhaps it should be. Fixing the kind to UNITSUM fixed it.

Now, I can rewrite that expression as:

K:UNITSUM = _min(LEN, N `- FIRST)

with

typedef fun n”_min” (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop (“_unitsum_min",(x,y),UNITSUM);

but if I use “min” instead of “_min” I get this:

[flx_bind/flx_lookup.ml:2973: E149] [lookup_name_with_sig] Can't find min[] of BTYP_array(BTYP_inst(102[]:TYPE),2)=
min[] of int^2
In /Users/skaller/felix/src/packages/io.fdoc: line 875, cols 14 to 17
874:
875: len := min(len1, len2);
****
876:

The problem is that typedef functions, do not overload. In fact a unique symbol goes
in the symbol table, if you write:

typedef fun f (x:TYPE):TYPE => x;

it actually means

typedef f = fun (x:TYPE):TYPE =>: x;

i.e. its a variable defined as a lambda, not a function.
So you can’t have both type functions and value functions of
the same name in the same scope. The decision not to overload
type functions may be right or wrong but it simplifies the type system.

So I am using this:

K:UNITSUM=_unitsum_min(LEN, N `- FIRST)

It would be “better” to use a class and explicit qualification but
that wouldn’t be so nice for `+, `* etc. That could in turn be
fixed in the parser …

Anyhow it works!

fun subarray[
FIRST:UNITSUM,
LEN:UNITSUM,
T,
N:UNITSUM,

K:UNITSUM=_unitsum_min(LEN, N `- FIRST)

]
(a:T^N) : T ^ K
=

{

var o : T ^ K;
for i in ..[K] do
var first = Typing::arrayindexcount[FIRST].int;
var outix = caseno i;
var inpix = (first + outix) :>> N; // checked at run time?
&o.i <- a.inpix;
done
return o;
}

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

[John Skaller2]

You can now write .. syntax may change due to inconsistency ..

static-assert 1 `< 2;

The result is nothing. If you write:

static-assert 2 `< 1;

you get a compile time assert fail. If you write:

static-assert 1;

it also fails since the kind of the type expression 1 is not BOOL,
a static bool.

It’s not implement yet but you can also write stuff like

static-assert (a:int, b:int) < (a:int);

which asserts the first record type is a subtype of the second one.

Assertions can be used in pv lists:

fun f[T, U where T < U] (x:T,y:U) => ….


which means T has to be a strict subtype of U. No idea if that’s useful.

I’m getting to two things. First:

val unix = TRUE;
val windows = FALSE;

At present Felix uses:

macro val unix = true;
macro val windows = false;

Then if you write

if unix do
blah;
else
blo;
done

macro substitution reduces the conditional to

if true do …

and then the macro processor does “code folding” and reduces the statement to

blah

But using macros sucks! Doing conditional compilation on the bases of
“I sure hope that expression reduces to a constant known at compile time”
sucks because if it isn’t a constant, the check ends up being done at run
time and both branches have to actually compile and link.

If we use a static bool it HAS to reduce at compile time. Unlike the macro
case however, both branches may get type checked (not sure yet).

A more advanced feature: user defined kinds.

kind OS = | UNIX | WINDOWS | MACOSX;
val os : OS = UNIX;

match is with
| UNIX => ….
…


looks more fun.


The OTHER thing I’m working on is a proper modelling of typesets.
In particular

int in ints

has kind BOOL. So int is kind TYPE, but typesets like int
are not being properly kinded yet because I’m not completely
sure what they are :)

By the way there is an annoying terminological issue:
values of kind BOOL, namely TRUE and FALSE are
said to be types. However they are NOT types of any expressions.



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

[John Skaller2]

>
> At present Felix uses:
>
> macro val unix = true;
> macro val windows = false;
>
> Then if you write
>
> if unix do
> blah;
> else
> blo;
> done
>

I had a go at this but there’s a problem: the idea was to bind the code first,
the throw out what fails the condition. Unfortunately, Felix desugars structure
away before binding. If/then/else is reduced to gotos. Desugar also splits
code into executable instructions or definitions.

For simple cases like above binding can be done early but for arbitrary
predicates on types it isn’t possible.



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

[John Skaller2]

Now the type language is split out, for expressions + and - have the same
precedence and * and / also. They’re now binary (not chained) operators.
For types + and * are chain operators.

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

[John Skaller2]

So now a difficult goal.

I want to make

match xx with | p1 => e1 | p2 => e2 .. endmatch

work for distinct kinds of xx, p’s and e’s. For example xx could be an
expression and e’s statements or expressions, or xx could be a type,
and e’s expressions, types or static bools.

Unfortunately, Felix desugars matches too early for binding the kinds.
We have at present:

match: EXPR -> EXPR
match: EXPR -> STATEMENTS
typecase: TYPE -> EXPR
typematch: TYPE -> TYPE

I want also match: TYPE -> BOOL because TYPE in TYPESET is a constraint
implemented by that.

Desugaring does two things. The first is that it splits statements up into
executable instructions and declarations. For variables the split is simple.
For functions, the declaration *contains* the executable instructions,
in other words, the desugaring introduces a new way to represent nested scopes
which separates executable code from the scope tree.

The second things desugaring does is lambda lifting. Lambdas are lifted out
by adding a new function to the containing scope then calling it.

The RHS of a pattern match branch is a kind of lamda, so all the branches
are turned into functions and the whole match is also turned into a function
so the branches can be nested in it. Then a if/goto chain is created to select
the branch in the top function.

Unfortunately this is NOT how type matches work, the logic is actually
much the same, but the implementation involves the compiler performing
reductions instead of saving the actions as executable instructions ..

so unifying matches is going to be hard.

In particular, its easy to calculate kinds from bound terms (expressions, types),
but above we want to use the bound kinds to determine HOW to bind the terms.

Recursion sucks :)



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

[John Skaller2]

I’m going to make some syntax changes.

Functions will no longer need = sign after the type unless there is an expect clause.

I want to rename “union” to be “variant”. Its too confusing talking of unions
when they’re discriminated and i actually want undiscriminated ones too.

Since prefix ! is only used in the type system, and infix ! is only in for
cons’ing lists in expressions, I am thinking to copy Swift and use

!optional

to mean

match optional with | Some x => x | None => abort program

In particular it could be useful for “possibly NULL pointers”?

I want to getr rid of

typematch .. with .. ?x .. => …

The ? there is not needed now in ordinary matches.

Also, i can now change the keyword to just match, it has to be
a type match if its in a type. I also noticed we have “subtypematcfh”.
Forget we had that!

Felix now calculates the kind of a match. So for example in the
type system

typematch x with | int => TRUE | _ => FALSE endmatch

has kind BOOL not TYPE.

Note that we still need

typecase expr with | ….

which is actually a type match on the type of expr, but it returns
an expression! The kinding system doesn’t help here!


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

[John Skaller2]

I have just commited two new tools which allow C++ to be autocompiled.
The are

flx_find_cxx_packages
flx_gen_cxx_includes

So what you do is make a C++ program with this near the top:

// @require package sdl2
// @require package sdl2_ttf

These are comments found by a regexp so the exact position isn’t critical.
This is ALREADY ENOUGH to ensure the program is correctly compiled
and linked by flx:

flx —c++ —static hello.cxx

*provided* you put the required #includes in. This has been working
for ages already.

Instead of manually putting the #includes in you can instead just add

#include “hello.includes”

Now you program will not compile. To fix it do this:

flx_find_cxx_packages hello.cxx | flx_gen_cxx_includes \
—path=build/release/host/config > hello.includes

Now your program compiles, links and runs .. it will work

ON ALL PLATFORMS

and

WITH THE SAME BUILD SCRIPT

provided of course you installed the libraries and set up the config database.
That only has to be done once (per library you install).

So clearly running those tools is not the right way, flx should do this step itself.
The question is, how to comand it to do so?

We can do it fully automatically, by putting the include file in the cache
and making sure it can be found. However that is OK for just running a program,
but its NOT ok for a normal C++ programmer.

An option like:

flx … —gen-include-file=hello.includes …

might be the right way. However few want to put the #includes in a separate file …

Ideas? The tech is there, its just a “UX” issue :)


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

[John Skaller2]

I just implemented type comparisons and got a big surprise :-(

This works correctly:

static-assert _typeop (“_type_lt”, ((a:int,b:int),(a:int)),BOOL);

Its true, (a:int, b:int) is a strict subtype of (a:int).

I got a diagnostic to show it happening:

Comparing
BTYP_record(a:BTYP_inst(102[]:TYPE),b:BTYP_inst(102[]:TYPE))
with
BTYP_record(a:BTYP_inst(102[]:TYPE))
got <

Cool! But the notation sucks so I do this:

typedef fun lt (a:TYPE, b:TYPE):BOOL => _typeop ("_type_lt", (a,b),BOOL);
static-assert lt ((a:int, b:int), (a:int)) ;

Actually I wanted to use < but the new grammar doesn’t allow that yet, will fix.

BUT:

It fails!!!!!! What???

Comparing BTYP_type_var(68472:TYPE) with BTYP_type_var(68473:TYPE) got =

It’s saying type variable a = b. Which is correct! More precisely

a <= b and b <= a


Why? Because trivially we can unify a with b by the assignment

a <- b

More easy to understand, these TWO assignments unify both terms:

a <- c
b <- c

So each is a subtype of the other so they’re equal.

In other words if you have a function like:

fun f[a]: a -> x

it should work for any argument, including another type variable.

The argument works both ways (swap a and b) hence .. the types are equal.

Obviously .. that argument is bullshit.
The types are unifyable .. not equal.

But that’s only the FIRST problem. The SECOND problem is that Felix got too smart,
and reduced the RHS of the typedef to TRUE. It didn’t actually replace a and b with
the type arguments. Because they’re gone I suppose.

What SHOULD have happened is that the reduction on definition failed,
leaving the _type_op as the RHS of the function, and then beta-reduction
of the type function when applied to the two record arguments, substituting
a and b away, finally allowed the typeop to be reduced to a static_bool
(namely, TRUE since it is). In other words it should have reduced first to

static-assert _typeop (“_type_lt”, ((a:int,b:int),(a:int)),BOOL);

and then to TRUE.


The PROBLEM is that subtype comparisons (whatever they’re for) are NOT
the same as a specialisation, because a specialisation, used to fix the type
variables in a function parameter, is directed, that is, the parameter has
dependent type variables (universals) that need to be fixed, whereas
the argument has independent (existential, or abstract) type variables,
which are not in the slightest variable! They’re just unknowns, but they
cant be messed with.

With subtype comparisons all the type variables are existential.
More precisely

T1 <= T2

works fine, by finding an MGU for the subsumption we reduce to a *monomorphic* subtyping
comparison because the RHS type variables are existentials NOT variables (abstract,
opaque, unknowns, or independent variables whatever you describe them as).

But you CANNOT conclude from

T1 <= T2
T2 <= T1

that T1 == T2, because you get two distinct unifiers. The only way to draw the
conclusion is to find a SINGLE unifier.

Of course the unification algo can do this trivially! You just solve

T1 <= T2
T2 <= T1

together, and discard the MGU. You can’t solve each separately, discarding
the MGU each time!




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

[John Skaller2]

So now I have to ask myself .. what am I trying to achieve?
In fact I implemented (mis-implemented) this just for fun, to get some extra kind level operations.

Here’s where the comparison routine is actually used at present:

When overloading we first find a set of candidates by name of the function.
Then we check if the the argument is a sub-type of the function parameter.
The check includes subsumption (type variables) as well as subtyping,
type equality (after subsumption) is allowed. The MGU is important because
it is used to generate an instance of the function with an exact match of
the parameter to the argument in two steps: first we substitute the MGU
into the parameter, and then we wrap the argument in a subtyping coercion.

From the set of candidate that match, we want the most specialised one.
If there is none, the overload fails. We pick one function as a start,
and then another to compare with. If the one we picked second is
a subtype of the first one, it is more specialised so we throw the
first one out and keep the second one.

If first one is more specialised than the second one, we throw
the second one out.

Otherwise they’re eithe equivalent or incomparable, and we have
to keep both.

Then we pick the next candidate and repeat, only now we have to
do the pairwise comparison with both the accepted candidates.
And we continue, comparing each new candidate with all the
accepted ones until we run out of candidates.

At this point, either we have one remaining most specialised
function or the overload fails.

For this, the “equality” relation that type variable A = B is correct.
The types aren’t equal, but they are equivalent.

The point here is that the actual argument matched with the two types
will produce distinct MGUs, but the result of substitution will be identical.
If the argument is C, then A <- C would be used for the A function and
B <-C for the B function.

Actually this is alpha-equivalence.

However in the “type_eq” case i expected equality not equivalence.
The reduction on the actual pair of parameters showed they’re
alpha-equivalent but that is irrelevant because they’re not going
to be equal after different types replace the A and the B variables.

In other words the “equals” I am using is “alpha-equivalence” not
equality.

Which leaves the issue of what to actually measure ..:-)



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

[John Skaller2]

Ughh.. Well ..

Let MT be the category of monomorphic types, objects are types, arrows are functions.
A functor F:MT -> MT is a structure preserving map. This means, for types A, B, C
and arrows f:A->B, and g:B->C, and h:A->C = f \odot g (the composite), if

A |-> FA
B |-> FB
C |-> FB

then

Ff: FA -> FB
Fg: FB -> FC
Fg: FA -> FC

AND

Ff \odot Fg = Fh

The notation is hard to read so here is the English translation:

A functor is a TRIANGLE PRESERVING MAP


A FA
|\ |\
| \ —————> | \
| \ | \
V V V V
B > C FV -> FC

So for example

List: MT -> MT

is a functor, where

’t -> ’t list

for all type ’t in MT. For example LIst int is a list of ints. We sometimes write
A simpler example is:

forall T . int * T

which could also be written:

lambda T. int * T

This is sometimes called polymorphic type. The point is, it is NOT a type,
its a functor from types to types.

Functors can be composed. For example, map each type T onto a list of T,
then map that onto an array, you get array of listr of T.

If there are two type variables we can use a bifunctor:

MT * MT -> MT

For example a tree, with one type decorating the leaves and another the nodes.
But we can also CURRY it:

MT -> MT -> MT

First, we map T to a tree with leaves of T and the node type not yet known,
so that is a functor, its the functor returned by the first step. Wrting again:

MT -> (MT -> MT)

This function doesn’t return a type but a functor. Its only when that is applied
that we get a tree with the leaf and node types both fixed. It CT this is called
a natural transformation, in programming a generic function.

The rule for natural transforms is similar to functors but the English translatrion is:

natural transforms are SQUARE PRESERVING MAPS

More precisely they preserve commiting squares. In fact if you make
a category whose arrows are functors on MT, the natural transforms
on MT are the functors on that category. CT is highly self-applicative :-)

So what’s this mean: well, the Felix category TYPE is actually
the category of *polymorphic types*, that is, functors on MT.
More precisely, functors on the collection 1, MT, MT * MT … MT^N,
however we can remove that mess by currying so we only have functors
of one variable. In lambda terms:

lambda T. lambda U. T * U

for example consists of two one step abstractions. The inner abstraction is
an ordinary functor. However the outer abstraction is abstracting a functor,
not a type. So the signatire is

MT -> MT -> MT

Now what all this means is that a type like

int * T

in Felix is rubbish because there’s no binder. We have to know if T is quatified
or not. If it is, its a polymorphic type, that is, a functor. Otherwise its a monomorphic type
which happens to contain an unknown type.

This is why my comparison is nonsense: there are no quantifiers. Felix doesn’t allow
standalone polymorphic types; In function:

fun sin[T]: T -> T

the argument isn’t polymorphic. Its the *function* that’s polymorphic.
In this:

variant list[T] = 1 + T * list[T];

list is not polymorphic, its NOT a functor .. its an INDEXED type.
list[T] is *monomorphic*. We just don’t know what T is. Let me show you:

typedef T = int;
… list[T] …

see? That’s just a list of int. You have to write:

fun list_f (T:TYPE):TYPE=> list[T];

and THAT is a functor. list is actually a type scheme.

So the problem is when I ask:

T < U

it isn’t enough to just give the polymorphic type expressions. if U is a function
parameter and T is the argument, then the type variables in U are dependent
variables that have to be instantiated to make T an actual subtype of U.

The unification engine in Felix takes a list of equations AND a set of dependent
variable names. It has to solve for the independent variables, returning the
solution, called the MGU. To decide if a function parameter P >= A, where
A is an argument, we alpha-convert the argument, then find the type variables
in the parameter and call unification demanding P >=A and a list of assignments
to the variables of P that make P a supertype of A.

if you ONLY want to know if X is a subtype of Y, the set of variables to be
set must be empty. The variables are just taken as unknowns. The same
variables can be present on both sides.

For example

(a:int, b:T) < (b:T)

In fact:

(a:U, b:T) < (b:T)

It doesn’t matter what I is here. But this is false:

(a:U, b:T) < (b:W)

because T < W is false. Were it true, then int < string would be true!
The point is THIS subtyping query has no subsumption.

Butr this won’t work in my code either because .. A ~ B is false
for ALL equality and subtyping. It is judged false *before* the type variables
are replaced.

Type matches do not have this problem! The logic there is that you can
only make a judgement in the presence of type variables if NO possible
subtitution can refute the judgment. So for example:

A < B

is neither true nor false but irreducible. Such a type expression always reduces
on monomorphisation though.

So this correctly asks if B subsumes A:

typematch A with
| B => TRUE
| _ => FALSE
endmatch

This works but doesn’t allow subtyping, only subsumption. This allows
subtyping too:

subtypematch A with
| B => TRUE
| _ => FALSE
endmatch

(yes, that exists in Felix!).

The point is the FALSE branch cannot be taken until there is NO substitution
of A and of B for which B matches A possible. For example:

typematch X * Y with
| U * V * W => ….

that branch can be immediately discarded. But this one cannot:

| Q => …

So actually I already know how to do it correctly, but I don’t see how it
can be done with type ops .. :)



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

[John Skaller2]

AHA! Now I remember what i am trying to do!

In Felix an “object” in the Java sense can specify it impements several
types. The rule is that the actual return type is a subtype of each of the specified
types. That ensures that any functions requiring any o fthe specified interfaces
will accept the object being constructed.

At present, this doesn’t work. At best for defined object constructors
(which are functions returning a record of closures), there was (still is? I forget)
a type equality check. AFAIK you can’t give a return type for an anonymous object.

For defined objects a static-assert return-type <= interface-spec is enough.
For anon objects a special function may be needed:

fun identity[T:TYPE, constraint:BOOL] (x:TYPE) => x;

which just returns its argument but ALSO checks tghe constraint
is satisfied and aborts the compilation otherwise. Then the subtyping
check can be used for anon objects too.

The point is that now the specified interface involves type variables of
the object constructor function, and the type of the return value does too.
So in this case we want to check subtyping but NOT allow subsumption.

So in the unification algo, the set of dependent variables passed (Dvars)
must be empty. We don’t want a unifier.

Here’s the problem: other calculations like the UNITSUM addition can’t
run until the type variables are replaced with actual values. But type comparisons
on polymorphic types can. The problem is type variables are used as parameters
for the types which could be polymorphic. So there’s no way to tell if the
parameters have been replaced yet. So the argument is always reducible.

The only fix is to wait until monomorphisation eliminates the type variables.
Which is what the other typeops do anyhow.

Note, this is NOT a problem with

_typeop(“_type_lt”, … ….

that works fine. The problem is the wrapper function.

//typedef fun lt (a:TYPE, b:TYPE):BOOL => _typeop (“_type_lt”, (a,b),BOOL);
^^^ doesn’t work

The funny thing is that this:

typedef fun le (arg:TYPE, param:TYPE):BOOL =>
subtypematch arg with
| param => TRUE
| _ => FALSE
endmatch
;

works just fine! Because the type match KNOWS when it is not yet
reducible.


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

[John Skaller2]

So here is the difference between C++ and Felix:

fun f[T] (x:T) {
static-assert (a:int, b:T) <= (a:T) ;
return x;
}

println$ f 1;

This FAILS in Felix. As it should.
Replace the assertion with:

static-assert (aT, b:T) <= (a:T) ;

and it works. In Felix the check is first done before monomorphisation.
The first assert fails, EVEN THOUGH there is a substitution of T
for which the assertion passes. The second check passes,
because there is NO possible substitution for which it can fail.


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

[John Skaller2]

So now, a bug. Here’s the problem: At present when you have a function parameter type P,
and and argument type A, Felix checks if

P >= A

That is, P is a supertype of A. Here “supertype” also means subsumption.

The problem is that it examines P for type variables and makes them all
dependent, then calls unification with that set. this means the MGU will
try to set those variables to parts of A.

The unification is correct. But chosing “all the variables in P” is a hack.
Its totally wrong! Here’s an example:

fun f[T] …
fun g[U] (x: U * T) …

The parameter type of g has two type variables in it, but ONLY U is a dependent variable
when seeing if an argument matches it. T is from the containing scope and we’re not
free to set it to instantiate g.

I think the key algo (overloading) does this right though.


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

[John Skaller2]

OK so this now works:

typedef fun le (a:TYPE, b:TYPE):BOOL => _typeop ("_type_le", (a,b),BOOL);
static-assert le ( (a:int, b:int), (a:int) );

There were TWO bugs

(1) The typeop constructor evaluated typeops.

For other typeops, that’s fine! All the others evaluate to their final result
eagerly if they can otherwise the term doesn’t reduce. Evaluation
“as soon as possible” was ok, because any lamba abstraction would
cause the evaluation to fail to reduce. Not so type comparisons!
[Also, the eager result, when found, would always equal the lazy result]

(2) Reduction of a type function application was done by first
reducing both the function and argument, the substituting, then
reducing the result. Normal order evaluation (lazy evaluation)
REQUIRES the substitution to be done first, then the result
reduced.

Felix always mandated normal order beta-reduction, but it didn’t
matter before.

The constructor no longer evaluates typeops, it just makes them,
and the beta-reduction routine now does normal order evaluation.
These two changes fixed the problem.

Amazing how actually implementing the maths works.. :-)

In case you didn’t follow any of that .. the problem was two fold:

first, the typeop in the first line got reduced to FALSE immediately by
the constructor, and, even if that got fixed, evaluating the function
in the beta-reduction routine in the application in the static-assert
cause it to be reduced *before* actually plugging the arguments in.
Again leading to FALSE.

The problem is that the _type_le function cannot tell it shouldn’t do a reduction
with just the a,b type variable arguments. In fact it should. It just shouldn’t
be evaluated before the substitution resulting from applying the le type function.


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