Compose operators

[weaversa]

I often write helper functions like the following:

rejigger : {a} (fin a) => [a*8][8] -> [a*64]
rejigger x = join (join (map reverse (groupBy`{8} x)))

I was looking through SIKE and was impressed to see that @linesthatinterlace implemented compose and arrow (a kind of reverse composition) defined as infix operators (unfortunately, Cryptol doesn't allow . as a name for an infix operator and >>> is already right rotate).

What do folks think about adding more general support for compose and arrow?

Just as a starter, here is the above function rendered using compose and arrow. I think when functions are chained along, features like this can make specs more readable.

(<--) : {a, b} (a -> b) -> a -> b
(<--) f x = f x
infixr 1 <--

(-->) : {a, b, c} (a -> b) -> (b -> c) -> a -> c
(-->) f g = \x -> g (f x)
infixr 100 -->

rejigger_compose : {a} (fin a) => [a*8][8] -> [a*64]
rejigger_compose x = join <-- join <-- map reverse <-- groupBy`{8} <-- x

rejigger_arrow : {a} (fin a) => [a*8][8] -> [a*64]
rejigger_arrow = groupBy`{8} --> map reverse --> join --> join

[brianhuffman]

For function composition, there's a really obvious choice if you're willing to consider non-ascii characters:

/** U+2218, ∘, RING OPERATOR */
(∘) : {a, b, c} (b -> c) -> (a -> b) -> a -> c
f ∘ g = \x -> f (g x)

[brianhuffman]

The F# language uses <| and |> as forward and reverse application operators; |> (at least) was commonly used in SML and some other ML dialects. So these might be good choices for infix application operators:

(<|) : {a, b} (a -> b) -> a -> b
(<|) f x = f x
infixr 1 <|

(|>) : {a, b} a -> (a -> b) -> b
(|>) x f = f x
infixl 2 |>

EDIT: fixed associativities

[linesthatinterlace]

There's arguments for both the regular composition operator and the "-->" one I defined that's described above, I think. Former is more usual.

When I am fiddling in Haskell I used pointfree.io a lot because I like the pointfree style, and hence wanting some simple elements of it. Advantage is clear I think - disadvantage is that it might be slightly higher level than Cryptol is really designed for in terms of abstracting from what you're actually doing to data.

Incidentally it would be quite good to allow more flexibility in terms of what you can use in an infix operator name. Haskell also has the syntax of backticks that allow any appropriate function to be made infix and that is quite useful for this sort of style too: e.g. when defining multiple operators on some finite fields, one often really want to write them infix.

[linesthatinterlace]

Oh: it is crucial with --> (or $ <| or whatever it gets called) that it has right-fixity (o/w has little purpose).

[brianhuffman]

Yes, of course. I'll edit my post to correct the associativity.

[weaversa]

@brianhuffman Will those operators interfere with Cryptol's polynomial expression? <| x^^2 + 1 |>?

[weaversa]

Oh..Cryptol just outright rejects <| and |> as infix operators. unexpected: <|. And I really liked that suggestion!

[brianhuffman]

I guess that's what I get for posting code that I didn't actually test :(

I always thought the polynomial syntax was kind of a wart on the language, and that was before I realized that it takes up two very nice operator symbols.

[weaversa]

I've used the polynomial syntax in dozens of specs that include LFSRs / checksums.

How about tilde? It looks horrible doesn't it. I think I'm willing to accept unicode, especially since the notion is to make specs look cleaner and easier to read (so what if they're harder to type).

(<~) : {a, b} (a -> b) -> a -> b
(<~) f x = f x
infixr 1 <~

rejigger_rev : {a} (fin a) => [a*8][8] -> [a*64]
rejigger_rev x = join <~ join <~ map reverse <~ groupBy`{8} <~ x

(~>) : {a, b} a -> (a -> b) -> b
(~>) x f = f x
infixl 2 ~>

rejigger_fwd : {a} (fin a) => [a*8][8] -> [a*64]
rejigger_fwd x = groupBy`{8} x ~> map reverse ~> join ~> join

And then there's the question of whether we want application AND compose (? I'm out of my league here on functional programming verbiage) ---

(<~~) : {a, b, c} (b -> c) -> (a -> b) -> a -> c
(<~~) f g = \x -> f (g x)
infixr 1 <~~

rejigger_revf : {a} (fin a) => [a*8][8] -> [a*64]
rejigger_revf = join <~~ join <~~ map reverse <~~ groupBy`{8}

(~~>) : {a, b, c} (a -> b) -> (b -> c) -> a -> c
(~~>) f g = \x -> g (f x)
infixl 2 ~~>

rejigger_fwdf : {a} (fin a) => [a*8][8] -> [a*64]
rejigger_fwdf = groupBy`{8} ~~> map reverse ~~> join ~~> join

[brianhuffman]

I don't think we would really miss polynomial literal syntax; you can implement a quite similar notation with ordinary Cryptol. Instead of

irreducible = <| x^^8 + x^^4 + x^^3 + x + 1 |>

we could have

irreducible = (X`{8} + X`{4} + X`{3} + X`{1} + 1)

with a library function X defined as

X : {n, w} (fin w, w >= n + 1) => [w]
X = 1 # (zero : [n])

[linesthatinterlace]

I've used the polynomial syntax in dozens of specs that include LFSRs / checksums.

How about tilde? It looks horrible doesn't it. I think I'm willing to accept unicode, especially since the notion is to make specs look cleaner and easier to read (so what if they're harder to type).

(<~) : {a, b} (a -> b) -> a -> b
(<~) f x = f x
infixr 1 <~

rejigger_rev : {a} (fin a) => [a*8][8] -> [a*64]
rejigger_rev x = join <~ join <~ map reverse <~ groupBy`{8} <~ x

(~>) : {a, b} a -> (a -> b) -> b
(~>) x f = f x
infixl 2 ~>

rejigger_fwd : {a} (fin a) => [a*8][8] -> [a*64]
rejigger_fwd x = groupBy`{8} x ~> map reverse ~> join ~> join

And then there's the question of whether we want application AND compose (? I'm out of my league here on functional programming verbiage) ---

(<~~) : {a, b, c} (b -> c) -> (a -> b) -> a -> c
(<~~) f g = \x -> f (g x)
infixr 1 <~~

rejigger_revf : {a} (fin a) => [a*8][8] -> [a*64]
rejigger_revf = join <~~ join <~~ map reverse <~~ groupBy`{8}

(~~>) : {a, b, c} (a -> b) -> (b -> c) -> a -> c
(~~>) f g = \x -> g (f x)
infixl 2 ~~>

rejigger_fwdf : {a} (fin a) => [a*8][8] -> [a*64]
rejigger_fwdf = groupBy`{8} ~~> map reverse ~~> join ~~> join

I think you want both application and compose: sometimes it is just worse to go totally pointfree.

I'm not quite sure what the right fixity levels should be, but iirc compose binds as tightly as possible and application binds as loosely as possible, in general, I believe, so I think that's 100 and 1 on the scale cryptol uses?

[weaversa]

Yes, 1 - 100 is the scale for both infixl and infixr I don't know why @brianhuffman put infixl 2...but he's a wizard so I trusted him.

[linesthatinterlace]

Some other functions that are from the Haskell prelude and are occasionally useful:

const : {a, b} a -> b -> a const x y = x

flip : {a, b, c} (a -> b -> c) -> b -> a -> c flip f y x = f x y

id: {a} a -> a id x = x

But you can go down a rabbit-hole with this stuff really.

[linesthatinterlace]

(Incidentally, a nice way to use <~ is with zipWith: zipWith (<\~) fs xs takes a list of functions, a list of values, and applies each function to each value. and produces a list of the result. Although of course that's just the same as [f x | f <- fs | x <- xs] which I think is more ideomatically Cryptol at present? But has the advantage that you can partially curry and apply zipWith (<\~) fs to lists.)

[linesthatinterlace]

Is partial applciation of infix operators currently possible -i.e. can I do something like (+2) to mean the function with type signature {a} (Arith a) => a -> a, which is \x -> x + 2?

[brianhuffman]

I don't know why @brianhuffman put infixl 2

Two reasons: First, Haskell does it that way with & and $ (reverse-application operator & has a higher precedence by 1). Second, I generally avoid having both left- and right-associative operators at exactly the same precedence level, because it can lead to ambiguity and/or parse errors.

[brianhuffman]

Is partial applciation of infix operators currently possible -i.e. can I do something like (+2) to mean the function with type signature {a} (Arith a) => a -> a, which is \x -> x + 2?

No, Cryptol doesn't have section syntax for infix operators. If it's something you'd like to see in the language, you're welcome to create a new ticket with the "language" tag.

As far as Cryptol programming idioms go, we have historically kept away from too much higher-order functional programming stuff. (Admittedly, we have taken some steps toward it with some of the more recent additions to the Cryptol prelude.) I think this has been primarily a good thing, considering that an important intended audience for reading Cryptol code is people with a background in math or cryptography who are not necessarily FP or PL experts. One of the things we tout about Cryptol is that the syntax looks a lot like traditional mathematical notation (while also being executable and having a precise semantics). Adding a lot of fancy higher-order functional programming stuff in the prelude, especially non-standard operator symbols, could jeopardize that. So it's probably best to be conservative about what we put in the prelude. We could probably be a bit more adventurous with optionally-imported libraries, though.

[linesthatinterlace]

I think that is probably a decent argument for making the symbol for composition, if you do add it, something like (∘), then? Something standardish.