kikofernandez / encore Goto Github PK
View Code? Open in Web Editor NEWThis project forked from parapluu/encore
The Encore compiler.
License: BSD 3-Clause "New" or "Revised" License
This project forked from parapluu/encore
The Encore compiler.
License: BSD 3-Clause "New" or "Revised" License
A polymorphic function / method does not allow to deal with a read and linear mode at the same time. The sharable
means, among other things, that it's not linear. In the current affine ParT paper, we allow linear Par[t] -> read Par[t] -> linear Par[t]
. This is safe from the concurrency perspective and allows to re-use container-like data structures from the runtime, saving on allocations.
I would like to be able to group things such as class Object : read TObject * linear LObject
and ensure that both traits satisfy the same interface (methods), so that I can dynamically dispatch based on their mode. For instance, the following example is not allowed:
read trait TObject
require val x : String
def foo() : unit
()
end
end
linear trait LObject
require var x : String
def foo() : unit
()
end
end
class Object : read TObject * linear LObject -- [ERROR in this line]
end
active class Main
def main(): unit
()
end
end
The error reads:
Conflicting inclusion of method 'foo' from trait 'TObject' and trait 'LObject'
In class 'Object'
I believe this is useful because Encore infects the modes from the inner to the outer, i.e. Par[read t]
makes the type of the ParT read Par[read t]
. This prevents me from writing linear Par[t] -> read Par[t] -> linear Par[t]
. Same with classes: a class needs to be moded or defined by its traits, which already posses restrictions on mixing and matching read
and linear
, because it cannot be both at the same time and dynamically dispatch (current status that I am aware of).
In the example at the beginning, I believe it would be useful if we can abstract the mode over the class. Enters the concept of theories:
A theory statically ensures that traits with different modes implement the same interface. Example:
theory TCommon[t]
require def foo(x: t): t
end
read trait RVector[t] : TCommon
require val arraySize : int
def foo(x: t): t
print("read")
end
end
linear trait WVector[t] : TCommon
require var arraySize : int
def foo(x: t): t
print("linear")
end
end
class VVector[t] : (RVector[t] * WVector[t]) ++ TCommon
...
end
active class Main
def main(): unit
example(new VVector(), new VVector())
where
fun example(v1: RVector, v2: WVector)
dynamicDispatch(v1) -- prints read
dynamicDispatch(v2) -- prints linear
end
fun dynamicDispatch(v : VVector): unit
v.foo()
end
end
end
Based on this, we could Par[WVector] -> Par[RVector] -> Par[VVector]
. From the ParT perspective, we can p >> fun (v : VVector) => v.foo()
because its trait theory
guarantees that the behaviour is allowed.
Notes to Kiko:
VVector
implement the required method, it's more useful to explicitly state what is common knowledge and what is not (as interfaces do in Java and other PLs)p : Par[VVector]
, I don't care about whether the ParT is linear or read, it's safe in any case! If we were to say p : Par[WVector]
, then we know that the ParT inherits the mode of the WVector
.linear Par[t] -> read Par[t] -> linear Par[t]
somehow without theories, then the idea of theories is still useful (although a bit less)The following example crashes the ParT:
import Task
import ParT.ParT
read class MyObject
val id : int = 0
def init(id: int): unit
this.id = id
end
def value(): int
this.id
end
def inc(): uint
EMBED (uint)
// safely cheating to increment the counter
#{this.id} = #{this.id} + 1;
END
end
end
fun generateObjects(number: uint): Par[int]
var p = empty[MyObject]()
for i <- [0..number] do
p = p ||| liftf(async(new MyObject(i)))
end
-- TODO: there seems to be an issue with >>, futures and the running closure.
-- this crashes the program.
p >> fun (m : MyObject) => m.id
end
active class Main
def main(): unit
for i <- extract(generateObjects(10000)) do
print("{}, ", i.id)
end
end
end
It is most likely something that we are not tracing correctly, given that we use a big number of futures in the ParT.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.