Compile errors for attempted mutations

[Brandon Barker]

I noticed that mutations to vars defined outside of a function do not seem to actually occur at runtime, but was a bit surprised to see that they also didn't generate a compiler error. I'm sure the situations is complex, just looking for some insight. Thanks! Here is an example:

var mutTest: int = 0;


fun addUp(x:int^4) : int = {
  mutTest = 1;
  var sum = 0;
  for i in x do
     sum = sum + 1;
  done
  return sum;
}


val xs = 1,2,3,4;
println $ "mutTest is " + mutTest;
val sum = addUp xs;
println $ "mutTest is " + mutTest;
val sum2 = addUp(xs);
println $ "mutTest is " + mutTest;

[John Skaller2]

There are TWO things going on here.

1. functions are not allowed to have side effects. There is no diagnostic
because its hard to enforce, and, you may WANT side-effects deliberately for
profiling and debugging. Or cheating :)

2. Felix guarrantees to eliminate non-parameter unused variables
AND their initialisers.

In your code, the result of calculating addUp is put in “sum” and “sum2”
but you don’t use the result. So the variables are eliminated along with
the initialisers .. in other words addUp is never called! So the side
effect never happens.

Change the code to:

val xs = 1,2,3,4;
println $ "mutTest is " + mutTest;

println$ addUp xs;

println $ "mutTest is " + mutTest;

println$ addUp(xs);

println $ “mutTest is " + mutTest;

so the result is used, and you get:

~/felix>flx y
mutTest is 0
4
mutTest is 1
4
mutTest is 1

======== RATIONALE ====================
The rationale for elimination is:

var thread-pool = make-thread-pool 4;
var clock = system-alarm-clock();
var socket = auto-connect stuff;

If you use these variables, they’re initialised. There is an overhead and semantic
impact. The system alarm clock, for example, requires a polling thread to be started.
So if you don’t use the variable, eliminating it and its initialiser eliminates the overhead.

If you take the address of a variable it is considered used, because Felix doesn’t
know what you’re doing with the pointer. Too hard.

There is a type of function called a generator:

gen rand: 1 -> int = “::std::rand()”;

A very common example is:

var it = iterator (1,2,3,4);
for x in it perform println$ x;

Iterators are generators, and they have internal state. Generators may have *internal* state.
They’re not allowed to have *side*-effects but they are allowed internal effects. in this case
the variable “it” holds the internal state.

Similarly, rand, the prototypical generator, has “internal state”. Of course, Felix doesn’t know
what internal state is.

In an expression *direct calls* to generators are lifted out so the remaining expression is
free of effects:

println$ rand ();

is replaced by

var tmp = rand();
println$ tmp;

The lifting is done to ensure the generator is called exactly once. For example
consider:

fun twice (x:int) => x,x;
var y = twice a;
…

If twice is inlined, the compiler is allowed to create the code:

y = a,a;

because expression a isn’t allowed to have side effects. But if a is a generator application

var y = twice (rand());

we do NOT want this:

y = rand(), rand();

Note that generators have the same type as functions so the lifting ONLY works
with direct calls. If you pass a generator as an argument to a higher order
function, it may not be lifted.

Generators were an ugly compromise. I’ve been trying to figure out a way to get
rid of them. The problem is entirely syntactic. Originally, Felix required procedures
for effects:

var r: int;
random &r;

which is a pain to write, and forces the introduction of a variable the programmer
has to dream up a name for, and which then pollutes the current namespace.
So the compiler does this automatically.



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

[Brandon Barker]

Aha, right, I should have seen that regarding elimination of the addUp calls. Thanks for the explanation - I got point 2 but still am a bit confused on point 1:

 functions are not allowed to have side effects. There is no diagnostic 
because its hard to enforce, and, you may WANT side-effects deliberately for 
profiling and debugging. Or cheating :) 

I'm probably understanding this wrong, but does this basically mean: side effects are not legal, but are not strictly enforced by the type checker - much like speeding on the highway in some parts of the world?

Iterators are generators, and they have internal state. Generators may have *internal* state. 
They’re not allowed to have *side*-effects but they are allowed internal effects. in this case 
the variable “it” holds the internal state. 

One thing I'm still wondering about is the internal state that functions can perform. When I hear "no side effects", to my understanding, this means "pure", including any state changes that occur outside of the return value. So I guess it might be said that Felix doesn't allow side effects except for internal state changes in functions, though I don't know as yet what these other side effects might be in Felix.

As a more minor consideration, I wonder if doing something akin to treating functions as a lightweight object might be achievable, that is, an object not unlike the Function classes (or traits) from Scala. This would in principle allow some embedding of state - I'm not suggesting coming up with a complex object model, though I can't pretend to know how complicated such an idea would end up being in practice. The benefit (if enforceable) is that if anything from an outer lexical scope appearing in a function definition could appear as a 'val' instead of a 'var', except for the the state attached directly to the "function object", which could be mutable. Then it might be possible to tell the type of something as being stateless or not, based on the presence of the attached state. I know the one thing that is easy is for a non expert like myself to make wild suggestions ;-). For debugging purposes, I imagine it might be possible to switch a flag on that says make the stateful and stateless types identical, though I certainly haven't fully appreciated the implications of that, and it would probably be a gross over generalization - after all, some code might end up depending on functions that have a "stateful type". So probably some sort of local annotation would be more desirable.

Originally, Felix required procedures for effects: 

Ah, when I was looking at an overview, it sounded to me as if procedures were something like your standard mutable functions and "regular" functions in Felix were pure functions, but it sounds like this has been collapsed down into just functions now. 

[John Skaller2]

> functions are not allowed to have side effects. There is no diagnostic
> because its hard to enforce, and, you may WANT side-effects deliberately for
> profiling and debugging. Or cheating :)
>
> I’m probably understanding this wrong, but does this basically mean: side effects are not legal, but are not strictly enforced by the type checker - much like speeding on the highway in some parts of the world?

FIRST:

There is currently no type system support for effects, although there IS a place to put them
if I ever figured out how to use it: the general form of a function type is:

Domain -> [Effects] Codomain

I have no idea if this is useful. Effects defaults to unit.

SECOND:

The true meaning of “no side effects” in function is that the compiler optimises code
based on the assumption there are no side-effects. It can do things like:

* reoder operations
* inline functions
* choose either eager or lazy evaluation
* eliminate functions returning constants and all calls to them

For example consider the expression:

(f a, g b, h c) . 1

This is a tuple with 3 components, and the . 1 at the end is the second projection.
[Second because zero origin .. ]

The compiler optimises this to:

g b

throwing out the tuple construction, and throwing out the evaluation of f a and h c.
If you put “debug prints” inside f, g, and h, the side effects for f and h will not
be seen, but the one for g may be (depending on whether you actually
use the result).

The compiler cannot do this optimisation in C++ because functions can have
side effects. Its legal. In Felix it is not allowed precisely to support this kind
of optimisation.

A type theorist would kill me but in Felix, performance comes FIRST.
We worry about semantics later. Find an good optimisation, do it,
then look for a theoretical justification.

There are other optimisations of course, this is just one.


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

[John Skaller2]

>
> One thing I'm still wondering about is the internal state that functions can perform. When I hear “no side effects", to my understanding, this means "pure", including any state changes that occur outside of the return value.

No. You can mark a function as pure:

pure fun f(x:int) => ….

but otherwise *unfortunately* perhaps, Felix functions, although they cannot have side effects,
CAN depend on variables.

The point is that during the evaluation of an expression, “no side effects” means that the variable
cannot change.

So can write this code:

var x = 1;
fun getx() => x;
println$ getx();
x = 2;
println$ getx();

and it will print 1 then 2. The function getx() is free of side effects but it is not pure.
Hence, we do not have referential transparency.

I call such functions “accessors” or “observers”. I don’t like the fact that pure and
impure functions are not introduced by distinct binders. Adding the “pure” adjective
is fine “in principle” but I find I never do it. I’d like to require something like:

observer getx() => x;
accessor getx() => x;
acc getx() => x;

or something but it needs to be intuitive. Maybe I should just allow

pure tan (x:double) => sin x / cos x;

Syntax matters. I can’t decide .. so i haven’t done anything about it.

Of course in theory, you could do even more, as is required for C++ lambdas:
if you want to depend on variables in context you should list them in the interface
of the function.

As a general comment there are lots of properties of various things and
often, even though in principle they’re independent, they’re coupled in
a programming language to avoid too much refinement.


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

[John Skaller2]

>
> One thing I'm still wondering about is the internal state that functions can perform. When I hear "no side effects", to my understanding, this means "pure", including any state changes that occur outside of the return value. So I guess it might be said that Felix doesn’t allow side effects except for internal state changes in functions, though I don't know as yet what these other side effects might be in Felix.

I need to add here: when binding a C library, typically there is no reasonable choice other than to follow the
C function interface. So for example

gen MPI_send : … = “MPI_send($1, $2, $3)”

Technically this is a procedure NOT a function, but we model it has a generator so at least the
compiler has *some* idea it might have side effects. In fact for C bindings you can usually
use functions:

fun MPI_send ….

because the compiler doesn’t know anything about what the function does, so it will just call it
and the side effects will happen. If you do this it will usually work just fine. The usual BUG is this one:

var error = MPI_send( .. );
.. forget to check error ..

Surprise! Nothing gets sent! If you want to ignore the error you have to do this:

C_hack::ignore (MPI_send ( .. ) );

C_hack::ignore is a procedure that does nothing, its defined by:

proc ignore[T] : T = “$1;”;

In other words it calls C++ to evaluate the argument. The compiler cannot see into
C/C++ bindings like this so it just does what it is told.


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

[John Skaller2]

>
> As a more minor consideration, I wonder if doing something akin to treating functions as a lightweight object might be achievable, that is, an object not unlike the Function classes (or traits) from Scala.

I’m not quite sure what you want here.

In Felix, functions are first class values. We won’t need any special type of object as in C++.
I don’t know Scala.

Functions, generators, and procedures are all first class. This means you can
can use them as values. They automatically bind to their lexical context on construction.

Functions and generators differ in one crucial aspect. In order that recursive functions
work correctly, function closures are cloned.

On the other hand, generators are not re-entrant so they’re not. This means that
any state in a generator is preserved between calls.

For example here is an array iterator:

gen iterator (x:int^10) () {
for i in 0 .. <10 perform yield x.i;
return -1; // off the end of the array!
}

var it = iterator (1,2,3,4,5,6,7.8,9,10);
again:>
var result = it(); // invoke iterator
println$ result;
if result != -1 goto again;

This works because the variable i in the iterator is preserved across invocations.
If you change the definition to “fun”, if it works at all, it will go forever because
a new copy of the function is created on each invocation. This is necessary
to ensure recursive invocations througth a variable work.

> This would in principle allow some embedding of state - I’m not suggesting coming up with a complex object model, though I can't pretend to know how complicated such an idea would end up being in practice.

It’s already implemented :-) Lexical closures are core language.

> Ah, when I was looking at an overview, it sounded to me as if procedures were something like your standard mutable functions and “regular" functions in Felix were pure functions, but it sounds like this has been collapsed down into just functions now.

there are three basic kinds of things here:

(a) functions
(b) generators
(c) procedures

In all three of these you can modify state and get away with it because the compiler doesn’t enforce the rules.
In princple, functions cannot have effects, generators can only have internal effects, and procedures
can do anything.

In practice, the rules aren’t enforced BUT optimisations ARE performed that depend on compliance.

Generators and functions are similar except:

(a) generators can yield a result then resume where they left off, state preserved
(b) generators are not re-entrant, functions are, so functions use a prototype object
which is cloned on every invocation to ensure they’re re-entrant

Generators and functions use the machine stack for the return address.

Procedures are UTTERLY different, they use a spaghetti stack which consists
of heap allocated frames linked by pointers. This is because procedures
can be *spawned* as threads or fibres.

Finally note this model seems expensive .. heap allocated stack frames??

Sure but Felix OPTIMISES remember! It uses a C function for a procedures
if it can. Or just inlines it.




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

[Brandon Barker]

So maybe this is out of scope or extremely difficult or undesirable, but would it be reasonable to:

Check that functions, or at least 'pure' functions, do not depend on variables (unless passed in as arguments, and I haven't looked into linear capabilities if any of felix yet, and how this might interact with call-by-reference issues). A pure function could still declare vars internally I imagine. I guess if there are not potential performance issues here, it seems like it may actually be good to have this as a default, and make impure functions the exception rather than rule, and annotate them with an "impure". If this is achieved, I think it actually puts Felix ahead in purity checking and overall purity compared to most languages out there today, with notable exceptions I can think of being Haskell and variants thereof such as Idris, and of course ATS.

 

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

[Brandon Barker]

This is good to know about! thanks 

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

[John Skaller2]

>
> So maybe this is out of scope or extremely difficult or undesirable, but would it be reasonable to:
>
> Check that functions, or at least ‘pure' functions, do not depend on variables

There are a couple of issues doing it.

(1) What about pointers??

to be explicit: is this function pure:

var x = 1;
fun f (p: &int) => *p + 1;
… p &x …

It depends on a non-local variable, x in the use example, but the address is
passed as an argument. More to the point:

var x = 1;
fun g (p: *int) () => *p + 1;
var h = g &x;
println$ h(); // prints 1
++x;
println$ h(); // prints 2

So clearly, the same function call, via the closure stored in h returns different results
depending on the value stored in x, so we’d have to say it isn’t pure even though
it only depends on its argument .. the argument p happens to be a pointer.

On the other hand

fun swap (p: &int, q:&int) => q,p;

is passed pointers but is clearly pure. The question is, exactly what is the rule
for purity?

What about a HOF (higher order functions) that calls another?
Does the purity of the HOF depend on its argument being pure?
In that case, how can we tell, since pure and impure functions currently
have the same type? [I could change that .. using the “effects” annotation]

(2) Felix has no “constants” (maybe it should have).

Originally I thought “val” was a constant, It isn’t addressable so you cannot assign to a val.

val x = 1;
x = 2; // ERROR
&x <- 2; // ERROR

But .. it isn’t constant, it CAN be assigned to:

val x = 1;

That’s an assignment. Only one is allowed but consider:

var i=1;
next:>
val x = i;
…
++i;
if i < 10 goto next;


You can see now, x isn’t immutable. This is a flat loop, the loop body isn’t a scope,
so its not a new x, its the same x each iteration, reset to a new value.

Given that .. how do you define

val pi = 3.14l
fun sinpi ( x: double) => pi * x;

Is sinpi pure?


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

[John Skaller2]

>
> Check that functions, or at least 'pure' functions, do not depend on variables (unless passed in as arguments, and I haven't looked into linear capabilities if any of felix yet, and how this might interact with call-by-reference issues). A pure function could still declare vars internally I imagine. I guess if there are not potential performance issues here, it seems like it may actually be good to have this as a default, and make impure functions the exception rather than rule, and annotate them with an "impure". If this is achieved, I think it actually puts Felix ahead in purity checking and overall purity compared to most languages out there today, with notable exceptions I can think of being Haskell and variants thereof such as Idris, and of course ATS.

Haskell isn’t pure. Its a lie. Haskell can do I/O hence, functions can have side effects.
Haskell people mistakenly believe monads can provide sequencing. This is incorrect.
Monads express a dependency, but that isn’t sequencing unless you add a evaluation
strategy rules (i.e. imperative programming).

You CAN do functional programming in Felix. But it is a primarily a language with
a special interest in control flow.

Just wait until you meet coroutines :)
Actually .. a small white lie .. procedures. They’re not. They’re actually coroutines.
I just didn’t tell you that.

Ok so linearity: Felix has “uniquness types” They represent first order contracts.
This means the compiler checks if you try to use a variable whose contents have
been moved out. What it doesn’t check is if you “cheat” using pointers. Hence
the type checking is only first order.

In Rust, the checking is second order.

I have doubts about Felix uniquness types. I think Rust got this right
and Felix didn’t.

In Rust, variables are unique by default and you have to explicitly say they’re
sharable. In Felix, they’re sharable by default, and you have to explicitly
say they’re unique.

I suspect the Felix method doesn’t work properly. The problem is that
what C/C++ call “rvalues” or “temporaries” are in fact unique, which is guarranteed
not by Uniq type, but because they’re anonymous. So a uniquness TYPE of values
is the wrong idea. The right idea is that *storage locations* can be unique, that is,
its only variables that matter, because only variables can be shared or not:
expression values cannot be shared, because they’re just the interface
between a function output and another function input, which is always 1-1.

The real problem here is syntax. Expression syntax is totally wrong for the
idea of moving stuff. Notionally a unique variable “goes out of scope” after
it is used so it isn’t visible.Its hard to imagine this visually with existing
language syntax.

Finally, YES it is possible to say functions are pure unless marked impure.
At the moment we have:

fun f …… // unspecifiy purity
pure fun f .. // specified pure
impure fun f // specified impure

For the unspecified one, the compiler could try to determine if its pure
or not. It might fail but that doesn’t matter.

For the pure case, the compiler can again check. If it is definitely
not pure, report an error. But what if the compiler can’t decide?
In that case, the annotation would be dangerous.

It could give a warning if it can’t decide and then assume “impure”.

The issues here are not trivial, especially when it comes to optimisations
that depend on purity.

Part of the problem is that you only get “referential transparency” of
expressions if ALL functions are pure. Already generators make a mess.



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

[John Skaller2]

So just an aside here: Felix has coroutines which are basically the same as threads except
they exchange control volutarily and synchronously. This done with channel I/O.
So it’s a weak version of CSP, or if you like Go, without any concurrency.

Now, one thing I’m trying to figure out is, when can some coroutines
be run concurrently?

Certainy if two coroutines are pure .. and that means that they only access data
through channel I/O .. then they can run at the same time (provided the channel
I/O is suitably serialised).

If I can get a workable model, then .. well, Felix will totally kill Go.
It has polymorphism and is a real language, and the communication model
is correct, whereas Go has a some SERIOUS faults in the design.


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

[Brandon Barker]

On Sat, Nov 17, 2018 at 10:27 AM John Skaller2 <ska...@internode.on.net> wrote:

>
> Check that functions, or at least 'pure' functions, do not depend on variables (unless passed in as arguments, and I haven't looked into linear capabilities if any of felix yet, and how this might interact with call-by-reference issues). A pure function could still declare vars internally I imagine. I guess if there are not potential performance issues here, it seems like it may actually be good to have this as a default, and make impure functions the exception rather than rule, and annotate them with an "impure". If this is achieved, I think it actually puts Felix ahead in purity checking and overall purity compared to most languages out there today, with notable exceptions I can think of being Haskell and variants thereof such as Idris, and of course ATS.

Haskell isn’t pure. Its a lie. Haskell can do I/O hence, functions can have side effects.
Haskell people mistakenly believe monads can provide sequencing. This is incorrect.
Monads express a dependency, but that isn’t sequencing unless you add a evaluation
strategy rules (i.e. imperative programming).

I haven't really been using Haskell long, but my impressions are that - yes indeed, it isn't really pure 

(though apparently earlier in its evolution in the very academic phase, it was).

"Pure" is a word that always seems to need qualification, but Haskell is more pure than most in that it seems it 

does a nice job of enforcing purity when outside of IO or State monads (or similar). Also free monads, I believe,

give a more graph-like approach that can be executed in a more flexible way (albeit with some overhead most likely).

 

You CAN do functional programming in Felix. But it is a primarily a language with
a special interest in control flow.

Just wait until you meet coroutines :)
Actually .. a small white lie .. procedures. They’re not. They’re actually coroutines.
I just didn’t tell you that.

Ok so linearity: Felix has “uniquness types” They represent first order contracts.
This means the compiler checks if you try to use a variable whose contents have
been moved out. What it doesn’t check is if you “cheat” using pointers. Hence
the type checking is only first order.

In Rust, the checking is second order.

I have doubts about Felix uniquness types. I think Rust got this right
and Felix didn’t.

In Rust, variables are unique by default and you have to explicitly say they’re
sharable. In Felix, they’re sharable by default, and you have to explicitly
say they’re unique.

I agree on the above points on pointers being tricky and these points regarding Rust. 

I've been sorely tempted to learn Rust, but ATS still seems far ahead of it in most everything 

that matters except tooling, and probably error messages (and probably something I'm forgetting - 

oh yeah, currently code readability, at least for me - ATS3 is aiming to address that I think). 

I suspect the Felix method doesn’t work properly. The problem is that
what C/C++ call “rvalues” or “temporaries” are in fact unique, which is guarranteed
not by Uniq type, but because they’re anonymous. So a uniquness TYPE of values
is the wrong idea.  The right idea is that *storage locations* can be unique, that is,
its only variables that matter, because only variables can be shared or not:
expression values cannot be shared, because they’re just the interface
between a function output and another function input, which is always 1-1.

The real problem here is syntax. Expression syntax is totally wrong for the
idea of moving stuff. Notionally a unique variable “goes out of scope” after
it is used so it isn’t visible.Its hard to imagine this visually with existing
language syntax.

Finally, YES it is possible to say functions are pure unless marked impure.
At the moment we have:

        fun f  …… // unspecifiy purity
        pure fun f .. // specified pure
        impure fun f // specified impure

For the unspecified one, the compiler could try to determine if its pure
or not. It might fail but that doesn’t matter.

For the pure case, the compiler can again check. If it is definitely
not pure, report an error. But what if the compiler can’t decide?
In that case, the annotation would be dangerous.

It could give a warning if it can’t decide and then assume “impure”.

The issues here are not trivial, especially when it comes to optimisations
that depend on purity.

Yes, I can see it is quite tricky. Perhaps as an intermediate step, a "force pure" or "force impure"

could be added to help users where warnings are issued, which I suppose 

might have performance or correctness tradeoffs, though I imagine that

"force impure" would likely be the safer option as it would make fewer assumptions, and performance

could be benchmarked in specific cases.

 

Part of the problem is that you only get “referential transparency” of
expressions if ALL functions are pure. Already generators make a mess.

 

I think this goes back to the Haskell discussion of how it handles IO/State vs other pure functions.

If the IO monad disappeared from haskell, then this would also be true there, I think. But within the IO monad,

say IO A, you have a value (call it 'a') - any pure functions operating on a would be referentially transparent,

or so my understanding goes. 

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





--
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.

--

Brandon Barker
brandon...@gmail.com

[Brandon Barker]

Agreed, seems like Felix could be a good alternative to Go, and was already thinking along those lines. "Go 2" seems to be addressing some issues like generic programming and adding something like typeclasses a bit, but on the fence still are:

1. Nil/null

2. No TCO

3. Several other things I'm forgetting since I read about all this a few months ago, but only having mutable vars is certainly high up on the list as I recall.

--
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.

--

Brandon Barker
brandon...@gmail.com

[John Skaller2]

> I haven't really been using Haskell long, but my impressions are that - yes indeed, it isn't really pure
> (though apparently earlier in its evolution in the very academic phase, it was).
> "Pure" is a word that always seems to need qualification, but Haskell is more pure than most in that it seems it
> does a nice job of enforcing purity when outside of IO or State monads (or similar). Also free monads, I believe,
> give a more graph-like approach that can be executed in a more flexible way (albeit with some overhead most likely).

Haskell has a nice type system, but what it types is weak.
That’s why they’re looking to add linear typing to it.
Because the purely function model is useless by itself.
I mean literally impossible to do anything. At the very minimum
you HAVE to have an imperative top level that says

READ DATA
DO CALCULATION
EMIT RESULT

The calculation can be purely functional, but there has to be an imperative
*drive* to trigger evaluation. Reactive programming is exactly the above
model with a loop. Designing this way is wrong, the problem is we have
the maths for functional programming but not imperative programming.

In Felix, we have functional code but we ALSO have coroutines.
A coroutine is roughly a function turned inside out. So coroutines
are imperative, but they’re also pure and have the “dual” properties
of functions.

The problem is integrating the two models. I have found how to do that.
(It took 20 years to understand the problem and a few weeks to solve it).

The real issue is tha functional types are extremely weak.
To handle transmissions you need session types, and these
are not equivalent to a finite state automaton, as basic functional types are.

So the real problem is finding a type system for coroutines.

BTW: the calculus is OLD. Its a cut down version of Hoares CSP.
Take CSP and replace concurrency with indeterminism and
you have coroutines. Only, in Felix, coroutines can share memory,
because only one can run at any time: events are totally ordered.


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

[John Skaller2]

>
> I agree on the above points on pointers being tricky and these points regarding Rust.
> I've been sorely tempted to learn Rust, but ATS still seems far ahead of it in most everything
> that matters except tooling, and probably error messages (and probably something I'm forgetting -
> oh yeah, currently code readability, at least for me - ATS3 is aiming to address that I think).

ATS is all about *refining* the types.

Felix is about *generalising* the types.

Integrating the two systems would be really cool,
the Licence is the main obstacle. Felix is FFAU: free for
any use, including commerical, attribution would be nice
but it is not required. The licence is liberal to *encourage* commercial use.

Also ATS2 at least went over the top. This is fair in a research language
but a mistake in a production language.

The original ATS could only handle dependent types based on integers.
So you could use it for checking array and list lengths. The algorithm
for that was well known and built in to ATS2.

But Hongwei wanted to go further and moved to an external solver, Z3.
This was a mistake I think. The problem is you can now have intractible
problems the solver either cannot solve, or takes too long to solve.

This is good research but my view is this: if the machine algorithm
is not constrained to something reasonable there is NO HOPE for
the human programmer to understand and design. A language MUST
have restrictions on complexity, even if this means a loss of expressivity
or even soundness, so the human can design stuff at all.

So Felix actually has axioms and theorems in the language.
It also has reductions which are theorems of the form

if you see this .. reduce it to that

For example:

reduce distrib[T] (x:T,y:T,z:T) => x * ( y + z) => x * y + x * z;

These axioms are only first order AND clearly if you’re not careful
reductions can lead to an infinite loop. There’s both a constraint
and a potential unsoundness, which together form reasonable
balance because I think this is just on the margin of programmer
comprehension.


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

[John Skaller2]

>
> The issues here are not trivial, especially when it comes to optimisations
> that depend on purity.
>
> Yes, I can see it is quite tricky. Perhaps as an intermediate step, a "force pure" or "force impure"
> could be added to help users where warnings are issued, which I suppose
> might have performance or correctness tradeoffs, though I imagine that
> "force impure" would likely be the safer option as it would make fewer assumptions, and performance
> could be benchmarked in specific cases.

Sure, but there are lots of issues and i can’t solve all of them by myself.

Another issue is totallity/strictness. You can annotate that too:

total fun f ( .. ) => ….

and you can also add pre and post conditions. You can even do Monads
in Felix. [And getting that to type correctly was a LOT of hard work!]

> I think this goes back to the Haskell discussion of how it handles IO/State vs other pure functions.
> If the IO monad disappeared from haskell, then this would also be true there, I think. But within the IO monad,
> say IO A, you have a value (call it 'a') - any pure functions operating on a would be referentially transparent,
> or so my understanding goes.

I’ve seen counter examples. In fact, I couldn’t get simple stuff like open a file
and read stuff to work: it typed correctly but failed at run time because the file
wasn’t open.

A simple example is a monad which does

a >>= b >>= c >>= …

and it happens to have unit type, then the evaluations can just be thrown out
because there’s only one value of type unit. So the idea dependency leads
to sequencing just isn’t right. Functional view:

F ( G () )

where G returns unit .. then F depends on G, but G doesn’t have to get evaluated
at all, so any real effects are lost. And there’s a way to do this for bool too:


let t = F (true)
and f = F (false)
in if ( G() ) then t else false

in other words, you can evaluate F *first*, then G. The fact F depends on G() doesn’t
enforce sequencing *precisely* because of the assumption of referential transparency.



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

[John Skaller2]

> On 18 Nov 2018, at 13:18, Brandon Barker <brandon...@gmail.com> wrote:
>
> Agreed, seems like Felix could be a good alternative to Go, and was already thinking along those lines. "Go 2" seems to be addressing some issues like generic programming and adding something like typeclasses a bit, but on the fence still are:
>
> 1. Nil/null
> 2. No TCO
> 3. Several other things I'm forgetting since I read about all this a few months ago, but only having mutable vars is certainly high up on the list as I recall.
>

The problem with Go is that the core design is wrong. Apart from utterly STUPID syntax
designed by morons that know nothing about syntax .. :)

There are two core faults.

1. Testing a channel. This is WRONG.
2. Go-routines aren’t garbage collected

In Felix you CANNOT test a channel. There is no such thing as “end” or
closing a channel. This is rubbish. It destroys the design. Channel are
synchronisation devices, they’re not “pipes down which you write data”.


In Felix, coroutines cannot deadlock. If they deadlock, they’re
unreachable. If they’re unreachable the GC reaps them.
If they’re reaped, they’re DEAD so they cannot deadlock
because they don’t exist. So you don’t need to kill coroutines,
in fact YOU CANT. Coroutines can suicide but they can’t be killed.

Coroutines can LIVELOCK. This means, there is an active coroutine
which statically COULD write on the channel another coroutine is hanging on,
but it dynamically choses not to.

The semantics of fibration have to be exactly right, and Go got it wrong.
Its a pity because the kernel go-routine swapping machinery is really good.

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

[John Skaller2]

I may have describe this before. A rough design is this:

1. each thread has a scheduler running coroutines.

This is what we have now. Coroutines within a thread have totally
ordered events. So shared memory is accessible without locks.
The channels are also not thread safe because they don’t need to be.

Threads can communicate with pchannels, these are technically
data structures called monitors. The clients of the monitor block
until there is a matching client. This means the whole thread blocks,
not just the fibre using the channel.

So the first job is to fix this. In principle, the fix is easy. Instead of actually
blocking, the coroutine is descheduled until there is a match. This is exactly
what happens right now with asynchronous I/O from timers and sockets.

There is a design issue with the async monitor thread though: each pthread
doing async I/O gets its own demux thread. The demux thread polls the OS
until the async device (clock or socket) is ready, performs the necessary I/O
or other operation, and then takes the coroutine of the async wait list, and puts
it back on the scheduler list.

There should only be ONE monitor thread IMHO. In particular this seems necessary
if we’re going to treat pchannel waits as async events: we have to move TWO coroutines
back onto TWO distinct schedulers, which is best done by a single thread.

Ok, so, now we CANNOT migrate coroutines from one pthread to another because
in general, shared memory access is done without locking, because coroutines
within one thread are serialised anyhow. There’s an issue, if one thread runs out
of work, others are overloaded.

So the idea is now: if we have a coroutines which is PURE, then it can be launched
as a PROCESS. The constraint here is that channel I/O has to be serialised
properly. So there is a price to pay.

The idea is pure coroutines get put into a single queue and a thread pool
yanks them out when it has an idle processor. However we can NOT just
use locks to wait for channel I/O because that locks up a processor.
With OS scheduling locks are good because it deschedules a thread
and lets another one run. That relies on an oversaturation of threads
to be efficient. Thread pools don’t work like that.

So what we have to do, when the pool process tries to do I/O,
is immediately bump it out of the thread pool and hand it over
to a special thread which serialises I/O requests.

The point of this is that the channels do NOT require a lock.
Because the channel matching etc is all done by a single thread,
and so is automatically serialised.

What DOES requires a lock is moving the coroutine out of the thread
pool onto the waiting for I/O list. And I THINK but I’m not sure this
can be done lock free: its a muliple producer one consumer list.

On the other hand the “ready to run” process list is multi-consumer,
single producer.


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

[Keean Schupke]

Hi John,

This is an interesting discussion, just to show I am still reading this :-)

I think types for coroutines are 'protocols' something like extended GADTs but I haven't had the time from the day job to really try this. Presumably they also have co-algebraic properties, compared with functions which are algebraic. I think you can fit a range of language features into those classifications, type-classes seem algebraic, modules coalgebraic; global state algebraic, local state coalgebraic, etc. 

I agree that going to Z3 for solving is the wrong direction. I think the type system itself needs to be decidable, but I am not against allowing more complex proofs, if the programmer outlines the proof steps, so I would look at proof checking not proof search, which should take linear time (in the number of proof steps).

I quite like Go, but after lengthy discussions I now think there is zero chance they will get multi-parameter type-classes (interfaces in Go are single parameter type-classes, because God's invariance means you can model them as subtypes or type-classes). This is because multiple-dispatch is a fundamental change to the language. I also thing they won't get proper generics without type-classes, and they have gone with something like the early C++ concepts drafts where requirement are specified by a contract where you write code that is never executed but used to drive requirements like 'addable', this is because they refuse to have operator overloading in Interfaces, and so had to introduce another parallel mechanism.

Shelby3 and I spent a long time discussing how multi-parameter type-classes do not work with existentials which we see as a big problem. There may be some sort of solution in open unions if used correctly. That is you require type-classes on inputs, but return unions from outputs.

Cheers,

Keean.

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