statebox / idris-stbx-core Goto Github PK
View Code? Open in Web Editor NEWCategory theoretic semantics of glued open Petri nets in Idris
Home Page: https://statebox.org/
Category theoretic semantics of glued open Petri nets in Idris
Home Page: https://statebox.org/
The problem we've encountered in a live coding session on 2019/10/03 is that we can't parameterize the FFI call over the function name:
Type checking ./Main.idr
idris: Foreign Function calls cannot be partially applied, without being inlined.
CallStack (from HasCallStack):
error, called at src/IRTS/CodegenC.hs:350:38 in idris-1.3.2-HavsjJD68mD4JhbQOwqxh8:IRTS.CodegenC
One possible solution would be to use type providers to generate the static FFI function descriptions from some structured text file, a-la https://github.com/ctford/flying-spaghetti-monster/
What: We want to build and document a very simple version of typed core that accepts TDefs as inputs, describing a FSM spec and a path, and returns a TDef as output, describing the codomain of the path.
Why: We have three cores atm. A ReasonML one, an Idris one and a PureScript one. This project will allow to replace the current firing function in the other cores with its idris formally verified version.
How: We have to:
Hook up TDefs and Typed core
Translate the FSM input, that now is given in a txt file, into a Tdef.
The Tdef format should be:
Input: (FSM spec, state, path)
In the core, use the FSM spec to build a graph and the free category on it.
Evaluate: id_state;path
Return: codomain of id_state;path
Output format should be a tdef containing the codomain of path or a typechecking error.
use sos to rebuild code on file save and regenerate docs, so that they always stay in sync
it would be nice to have also examples of morphisms between Petri nets and even functors from and to the category of Petri nets
In FSM core, we provide instructions to build a path category for a FSM (call it C), together with a list of edges that we want to verify making a path in C.
At the moment we are doing so by relying on the fact that C, being a path category, has paths as morphisms. As such, we are relying on the inductive definition of path do work things out.
This approach will not generalize to other categories. For instance, in the hypergraph case we won't be able to do anything of this sort since we don't have an inductive data structure representing string diagrams.
So we need to develop a technique to tackle this more general problem:
Given a category C, and a list of morphisms for C, verify if you can lift this list to a valid morphism in C
For instance, if C has objects a, b, c, ... then [f: Mor a b, g: Mor b c]
can be lifted to a valid morphism compose C a b c f g
, while [f: Mor a b, g: Mor x y]
cannot.
A pre-net is just a net where places and transitions are indexed, e.g. by
Plan is the following:
Jelle:
add a
.travis.yml
and have the CI run this... I already created a docker image that can run latex and has pandoc so that it can create HTML with mathjax
desired build targets:
Inn
You give me two morphisms f, g such that domain of g is a permutation of codomain of f, with no repeated generators. I will use #36 to figure out how to turn one into the other and #37 to give you the composition of f and g.
copied from statebox/idris-ct#19
Currently, FSMs are specified by
Parsing files like fsm.txt.
Hardcoding typedefs:
idris-stbx-core/src/Computer/EcommerceExample.idr
Lines 43 to 65 in a2235af
Hardcoding type annotations:
idris-stbx-core/src/Computer/EcommerceExample.idr
Lines 127 to 138 in a2235af
Hardcoding FFI functions:
idris-stbx-core/src/Computer/EcommerceExample.idr
Lines 67 to 125 in a2235af
What we want is to express these in terms of Typedefs, so we can use that as a serialisation format.
WIP: PR #51
# run a bunch of steps in one go
./exec --fsm ./myProcess.fsm
--ffiMap ./myProcess.ffiMap
--types ./myProcess.tdefs # we don't have this, _but_ it's doable
--firingSequence ./myFiringSequence.txt
contents of myFiringSequence.txt
: suppose the type of transition “0” = boolean
the text between ()
= serialized terms of the corresponding typedef
0 (true)
1 ()
2 ()
2 (12)
3 ()
1 ()
4 ()
what to do with this “messageData”? very simple, just pass it to the FFI
(right now, the format is text based, s-expr), but in the future it will be some for of binary data, CBOR, or cap-n-proto
possible FFI call
printHello : () -> IO ()
~ prints ‘hello’printNumber : Nat -> IO ()
~ print ‘nr = »nat«’printBoolean : Bool -> IO ()
~ print ‘bool = …’f : A -> B
, X
is the typedef label on f
then, ffi call type = X * A -> B
given a category and an endofunctor, define the Kleisli category
Parts of this codebase have been factored out into https://github.com/statebox/idris-ct. This is now a dependency of the current repo (idris-statebox-core), and should be incorporated into the CI builds as such.
You give me two lists such that one is the permutation of the other. I give you a list of binary swaps which turn the first list into the other.
copied from statebox/idris-ct#17
As a user I want to try out the FSM execution. It would be nice to have:
The firing of a transition in a category FSMC(o,m,source,target)
(see #2 for details) can be represented as a function
t : GenMor(FSMC(o,m,source,target)) -> state : Mor(FSMC(o,m,source,target)) -> tokens : Obj(FSMC(o,m,source,target)) -> Mor(FSMC(o,m,source,target))
Morally, you give me the current state
of the net (represented by a string diagram), a transition t
(which is a generating morphism in the category) and the tokens on which you wanna fire it, tokens
(details missing here!) and I give you the next state by postcomposing t
with state
as specified by tokens
. Clearly this thing should be defined only for suitable t
, state
, tokens
.
There is a slight problem here: Suppose I have state:
A x A x C x B x C x D
and I want to fire a transition t: A x D -> C
using the second A
and the only D
in the state. To make this work:
A
and D
come together and we can apply t
. We want to do this in a "canonical" way (meaning that we want to find a way to do this that works in the same way for any possible enabled transition in the state).A(1) x A(2) x C(1) x B x C(2) x D
to A(2) x D x A(1) x C(1) x B x C(2)
(I am using numbers to distinguish copies of the same generating object). This means that the tokens that have to be used are rearranged to become the first in the product.
t : GenMor(FSMC(o,m,source,target)) -> state : Mor(FSMC(o,m,source,target)) -> tokens : Obj(FSMC(o,m,source,target))
and I give you a list of symmetries tensored with identities that can be sequentially composed with state
to reshuffle the object in its target as we want. In our example this effectively maps state
, having codomain A(1) x A(2) x C(1) x B x C(2) x D
, to state'
having codomain A(2) x D x A(1) x C(1) x B x C(2)
.state'
with t x id_A x id_C x id_B x id_C
and obtain the state representing the firing of t
in state state
using tokens tokens
.t
tensored with identities as in point ii.Note: If our nets are safe then we don't need to specify tokens
in our function. This is because in a product all objects will be different: For instance in our example A(1) x A(2) x C(1) x B x C(2) x D
represents having 2 tokens in A
and two in C
, which is not possible if the net is safe.
You see then that in a safe net a possible state is a product of objects X_1 x X_2 x ... x X_n
where all the X_i
are generating objects different from each other. In such a situation, if you give me a transition t
, two things can happen:
t
are present in the codomain of state
. In this case there is only one possible way to reshuffle the tokens in the codomain of state as specified above to compose with t
.t
are not present in the codomain of state
. In this case t
is not enabled in state
and so our stuff shouldn't typecheck.Provide an overview of the project, with step which needs to be taken and code snippets to guide the implementation
We should split our work in FSM-oracle into it's own project importing both Typedefs
and Idris-ct
since it doesn't particularly uses any of the rest of the Statebox-core.
It will also allow us to package the project in a distributable way such that people can test, play around and appreciate.
# run a bunch of steps in one go
./exec --fsm ./myProcess.fsm
--ffiMap ./myProcess.ffiMap
0 1 2 2 3 1 4 # depends on the FSM
myProcess.fsm
contains a specification for a graph, it can just be a file with a list in itmyProcess.ffiMap
defines to which ffi call we have to map each edge of the graph. the FFI calls can be hardwired for now, NP()
to ()
Using the generalize-graph
branch for the idris-ct
repo and the generalize-graph
branch in idris-stbx-core
repo, trying to compile the Computer/ComputerC
module the following error is reported
./Computer/ComputerC.lidr:84:75-79:
|
84 | > compute graph {initialVertex} {finalVertex} functor path initialValue = ?asdf
| ~~~~~
When checking deferred type of ComputerC.ComputerC.asdf:
Type mismatch between
extCompose (Ty [] a9) (IO (Ty [] b10)) (IO (Ty [] b10)) f11 (MkExtensionalTypeMorphism id) = extCompose (Ty [] a9) (IO (Ty [] b10)) (IO (Ty [] b10)) f11 (MkExtensionalTypeMorphism id)
and
extCompose (Ty [] a9) (IO (Ty [] b10)) (IO (Ty [] b10)) f11 (MkExtensionalTypeMorphism (\x => io_bind (io_pure x) id)) =
extCompose (Ty [] a9) (IO (Ty [] b10)) (IO (Ty [] b10)) f11 (MkExtensionalTypeMorphism id)
trying to debug this, it probably has something to do with the definition of the left identity of the Kleisli category: https://github.com/statebox/idris-ct/blob/1efb34427f9d664288055234de84b6d548292806/src/Monad/KleisliCategoryHelpers.lidr#L32
In a free smc, you give me two morphisms f g such that the codomain of f is a permutation of the domain of g. You also give me a list of binary swaps to turn one into the other. I will figure out for you a list of morphisms h_1, ..., h_n such that each h_i has the form id tensor symmetry tensor id, and such that the composition f;h_1;..;h_n;g makes sense. Said composition is what I will give you back.
copied from statebox/idris-ct#18
During the Summit, @clayrat, @marcosh and @epost found that the compiler-generated JavaScript wasn't usable with our existing code. What we want is for idris
to generate a (CommonJS) module that we can include and use from other code.
idris
to generate sensible js output.At the moment we are able to define graphs in files and turn them into FSMs in the Idris core. This is the bare minimum functionality we need in the current core that runs on the cloud.
So we can start endeavors to replace the current core with the idris one and see what happens.
Like #38 but now we allow repeated generators in the object. The users should be able to specify if they want the same generators to be swapped, and how. If they do not specify anything, then fastcompose should compose f and g without swapping the same object. This is analogous to "swapfree" symmetries in https://arxiv.org/abs/1904.12974 .
I know this specifications suck a bit, but they are a starting point to make clear what is that we want to achieve conceptually :)
copied from statebox/idris-ct#20
so this discussion
@FabrizioRomanoGenovese can you put in the stuff you discussed in the earlier meeting
We will have to consider this at some point, so I thought it would be good to put this out here.
Working on https://github.com/statebox/idris-stbx-core/tree/cartographer branch
convert all files to literate Idris and setup commands to generate code and documentation
To do this we need to define isomorphisms first. The current existential definition of isomorphism may be difficult to implement, so I was thinking about defining its constructor as something similar:
inverse: (a,b : obj cat) -> (f : mor cat a b) -> (finv : mor cat b a)
lawleft: (a,b : obj cat) -> (f : mor cat a b) -> (inverse f) -> compose a b a f (inverse f) = identity a
lawright: (a,b : obj cat) -> (f : mor cat a b) -> (inverse f) -> compose b a b (inverse f) f = identity b
I'm not sure this is the right insight so any comment is appreciated (also I am not sure it would compile!)
in https://github.com/jameshaydon/smproc there is defined a monoidal category. Integrate it with out definitions
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.