# 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 it
• myProcess.ffiMap defines to which ffi call we have to map each edge of the graph. the FFI calls can be hardwired for now, NP
• the following string of numbers is specifying the transitions to be fired
  Executing this thing should return error if morphisms are not composable or the outputs of all the executed functions if they are. For now it is ok to have FFI functions from () to ()

Provide an overview of the project, with step which needs to be taken and code snippets to guide the implementation

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

convert all files to literate Idris and setup commands to generate code and documentation

# 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

https://github.com/statebox/idris-ct

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

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:

• pdf
• latex -pandoc-> html
• compiled code (library)?
• compiled code (js bundle)? would be very noice to have
• html from idris doc tool? (buggy, see typedefs/typedefs#99)

As per this @wisnesky comment, we could try to hook up this project with AQL

https://github.com/jameshaydon/smproc
https://github.com/jameshaydon/cospanProc/

given a category and an endofunctor, define the Kleisli category

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

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.

Currently, FSMs are specified by

1. Parsing files like fsm.txt.

2. Hardcoding typedefs:

   idris-stbx-core/src/Computer/EcommerceExample.idr

   Lines 43 to 65 in a2235af

   	-- type definitions
   	-- these must coincide with the ones defined in tdefs.txt
   	Natural : TNamed 0
   	Natural = TName "Natural" $ TMu [("ZZ", T1), ("SS", TVar 0)]
   	InitialState : TNamed 0
   	InitialState = TName "InitialState" $ T1
   	ProductId : TNamed 0
   	ProductId = TName "ProductId" $ TSum [T1, T1, T1, T1]
   	Quantity : TNamed 0
   	Quantity = TName "Quantity" $ wrap Natural
   	CartItem : TNamed 0
   	CartItem = TName "CartItem" $ TProd [wrap ProductId, wrap Quantity]
   	CartContent : TNamed 0
   	CartContent = TName "CartContent" $ TMu [("NilN", T1), ("ConsN", TProd [weakenTDef (TApp CartItem []) 1 LTEZero, TVar 0])]
   	InvoiceId : TNamed 0
   	InvoiceId = TName "InvoiceId" $ wrap Natural

   .

3. Hardcoding type annotations:

   idris-stbx-core/src/Computer/EcommerceExample.idr

   Lines 127 to 138 in a2235af

   	edgeAsMorphism : (Fin lenV, Fin lenV, String) -> Maybe (mor' $ ioClosedTypedefsKleisliCategory FFI_C)
   	edgeAsMorphism (_, _, label) =
   	if label == "login" then Just ( (unwrap InitialState)
   	** (unwrap CartContent)
   	** MkExtensionalTypeMorphism login)
   	else if label == "addProduct" then Just ( (unwrap CartContent)
   	** (unwrap CartContent)
   	** MkExtensionalTypeMorphism addProduct)
   	else if label == "checkout" then Just ( (unwrap CartContent)
   	** (unwrap InvoiceId)
   	** MkExtensionalTypeMorphism checkout)
   	else Nothing

4. Hardcoding FFI functions:

   idris-stbx-core/src/Computer/EcommerceExample.idr

   Lines 67 to 125 in a2235af

   	-- functions
   	readIntFromUser : String -> IO Int
   	readIntFromUser = foreign FFI_C "readInt" (String -> IO Int)
   	intToProductId : Int -> Either () (Either () (Either () ()))
   	intToProductId i = assert_total $
   	let remainder = mod i 4 in
   	if remainder == 0 then Left ()
   	else if remainder == 1 then Right $ Left ()
   	else if remainder == 2 then Right $ Right $ Left ()
   	else Right $ Right $ Right ()
   	weakenNat : Mu [] (TSum [T1, TVar FZ])
   	-> Mu v (TSum [T1, TVar FZ])
   	weakenNat (Inn (Left ())) = Inn (Left ())
   	weakenNat (Inn (Right r)) = Inn (Right (weakenNat r))
   	generateRandomInt : () -> IO Int
   	generateRandomInt = foreign FFI_C "generateInt" (() -> IO Int)
   	generateInvoiceNumber : IO Nat
   	generateInvoiceNumber = cast <$> generateRandomInt ()
   	natToNatural : Nat -> Ty [] (Typedefs.wrap Natural)
   	natToNatural Z = Inn (Left ())
   	natToNatural (S n) = Inn (Right $ natToNatural n)
   	readQuantityFromUser : IO $ Ty [] (Typedefs.wrap Natural)
   	readQuantityFromUser = do
   	intFromUser <- readIntFromUser "quantity"
   	pure $ natToNatural . cast $ intFromUser
   	readProductIdFromUser : IO $ Either () (Either () (Either () ()))
   	readProductIdFromUser = do
   	intFromUser <- readIntFromUser "product"
   	pure $ intToProductId intFromUser
   	unwrap : TNamed 0 -> TDef 0
   	unwrap (TName _ def) = def
   	||| login just creates an empty cart
   	login : Ty [] T1 -> IO $ Ty [] (unwrap CartContent)
   	login () = pure $ Inn (Left ())
   	||| add product asks the use for a product id and a quantity,
   	||| and adds it to the cart
   	addProduct : Ty [] (unwrap CartContent) -> IO $ Ty [] (unwrap CartContent)
   	addProduct cartContent = do
   	productId <- readProductIdFromUser
   	quantity <- readQuantityFromUser
   	pure $ Inn (Right $ ( (productId, weakenNat quantity)
   	, cartContent))
   	||| checkout generates a random invoice id
   	checkout : Ty [] (unwrap CartContent) -> IO $ Ty [] (unwrap InvoiceId)
   	checkout (Inn cartContent) = do
   	randomNat <- generateInvoiceNumber
   	pure $ natToNatural randomNat

What we want is to express these in terms of Typedefs, so we can use that as a serialisation format.

WIP: PR #51

• un-hardcode types in edgesAsMorphisms
• graph should be a Typedef
• ...

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.

• Summarise current output format of idris compiler
  • format 1 (browser): TODO
  • format 2 (node): TODO
• Describe in what way these formats are not what we need. (We need (CommonJS) modules).
• Consider solutions
  • Patch idris to generate sensible js output.
  • Use a bundler? (Jelle's suggestion.)
  • Other?

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:

• The state must be reshuffled. That is, we have to recursively apply symmetries so that the second 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).
• My suggestion is: We go from 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.
  1. There should be a precise algorithm to do this. I think I can draft it if you want. This algorithm works like this: You give me 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).
  2. At this point we can compose 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.
  3. A transaction in the blockchain then can be specified by giving the symmetries produced at point i. and 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:

• All objects in the domain of 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.
• Some object in the codomain of 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.

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/

in https://github.com/jameshaydon/smproc there is defined a monoidal category. Integrate it with out definitions

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.

• uncurrying for type constructors
• invalid field indexing for functor
• erasure of recursive structure on Inn

use sos to rebuild code on file save and regenerate docs, so that they always stay in sync

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.

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.

We will have to consider this at some point, so I thought it would be good to put this out here.

A pre-net is just a net where places and transitions are indexed, e.g. by $p_1, \dots, p_n$ and $t_1, \dots, t_n$. These will be useful because probably using the full-flagged power of ExPetri will be a bookkeeping nightmare: Petri nets present free symmetric monoidal categories plus some nasty axioms expressed in terms of natural transformations. On the contrary, pre-nets just present free symmetric monoidal categories. This is because the indexing of places and transitions gives a canonical way to define generators in the corresponding Free SMC.

Plan is the following:

• Define a pre-net as a petri net built from a couple of finsets representing indexing of places/transitions.
• Define morphisms of pre-nets as usual
• Prove that these form a category and that it is a subcategory of Petri.
  All this stuff is mathematically trivial (there's a forgetful functor from Petri to Pre Nets) but may prove nasty in Idris.

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!)

Working on https://github.com/statebox/idris-stbx-core/tree/cartographer branch

it would be nice to have also examples of morphisms between Petri nets and even functors from and to the category of Petri nets

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

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.

• Open source idris-ct to make this possible? Not sure this is necessary but we do plan to do that soon.
• Activate the idris-ct repo on Travis.
• Incorporate idris-ct into this repo's build.

As a user I want to try out the FSM execution. It would be nice to have:

• clear installation/compilation instructions
• readme/minimal document that explains
  • how to specify a state machine
  • how to specify typedefs labels
  • how to specify calls in the target category
  • how to execute the state machine

so this discussion

@FabrizioRomanoGenovese can you put in the stuff you discussed in the earlier meeting

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