Jets

[uncomputable]

Assign a Simfony type signature to each Simplicity jet. The Simfony signature can be arbitrarily different from the Simplicity signature, as long as the compiler can convert between the two. In this commit, I chose signatures that are structurally equivalent, so no conversion is necessary. The equivalence is asserted in a unit test.

Nonstandard tuples

Simfony converts arrays and tuples into binary trees and always prefers the left branch. For instance (a, b, c) becomes ((a, b), c). This is what I call a "standard tuple". Simplicity sometimes prefers the left branch, sometimes the right branch. (a, b, c) can become (a, (b, c)), which I call a "nonstandard tuple".

For example, there is the Simplicity jet maj1: 2 × (2 x 2) which becomes fn maj1(a: u1, b: (u1, u1)) in Simfony. fn maj1(a: u1, b: u2, c: u3) would be more natural, but it requires a conversion.

I think the preference of the left or of the right branch comes from the way how the jets are nested as fully expanded Simplicity expressions. Always preferring the left branch might lead to larger expressions and other problems. In this case, it seems best to update the Simfony signature of the affected jets and to teach the compiler to insert a converter expression between the arguments and the actual jet (in a future PR).

Type constructors

Methods from <AliasedType as TypeConstructible> cannot be imported. These methods also require AliasedType as a parameter, so we cannot write AliasedType::option(U1) but we have to write AliasedType::option(U1.into()). jets.rs is prefixed with methods that take A: Into<AliasedType> as paramater, so we can write option(U1). The prefix AliasedType:: is also omitted. I am not sure if we should update TypeConstructible to include A: Into<AliasedType>.

Allocation vs const

I would like the jet source and target types to be compile time constants. However, this is currently not possible because types consist of Arcs. Without lazy_static, we have to generate the types from new every time and return a vector of them. Not ideal, but maybe acceptable.

[roconnor-blockstream]

In the Haskell term language, it is (kinda) right associated:

https://github.com/BlockstreamResearch/simplicity/blob/master/Haskell/Core/Simplicity/Term/Core.hs#L77-L82

i.e. s &&& t &&& u : A ⊢ B × (C × D) where (&&&) is the infix version of pair.

I don't think there is any particular reason of this choice, beyond that it is the associativity that the (&&&) operator from Haskell's Control.Arrow module does.

(Unlike the right associativity of (>>>) (i.e. infix comp) which is deliberate because right associating compositions can reduce the memory use of the Bit Machine.)

[uncomputable]

Ok, I chose left-associativity for Simfony without giving it much thought, simply because left comes before right. We can easily change Simfony to right-associativity.