Whither =>

[AssemblyZig]

It appears that one can create a simple type specification without constraints thusly: foo : {a} a -> a
And one can create a type specification with constraints: foo2 : {a} (fin a) => a -> a
But it is an error to include => when there are no constraints (e.g., foo3 : {a} => a -> a). (It is similarly verboten to elide the => when there are constraints -- as it should be.)

Any reason that the seemingly descriptive foo : {a} => a -> a is poor form?

[yav]

It is just that => is a binary operator, so it needs a left and right hand side. It is similar to not allowing things like foo : -> Integer

The following works, though, if you'd like to write an empty context:

f : {a} () => a -> a
f x = x

[WeeknightMVP]

To see that => is a binary operator, consider a curried type constraint:

module OneTimePad where

/** Encrypt plaintext `pt` using pre-shared key `psk` */
encrypt :
    {k, m}
    fin k  =>  k >= m  =>  // two  `=>`s!
    String k -> String m -> String m
encrypt psk pt = ct
  where
    ct = (take`{m} psk) ^ pt

OneTimePad> :h encrypt

    encrypt : {k, m} (fin k, k >= m) =>
                String k -> String m -> String m

Encrypt plaintext `pt` using pre-shared key `psk`

Interestingly, the interpreter reports type constraints in the usual uncurried form.

[jpziegler]

I agree that this is confusing to new users. (And, to some extent, veterans.)

There are up to three sections to a type definition:

• Type variable declarations, e.g. {a}
• Type constraints, e.g. (fin a)
• and the Type, e.g. a -> a

The first two are optional. Evidently, when type constraints are included, an operator is needed to apply them to the type.

When there is only a type variable declaration with no constraints, why is no operator required to "apply" the type variable declarations to the type?

At first, I was thinking that the => was needed so the parser could tell whether the parentheses were type constraints or a tuple parameter.

But that would be an issue for curly braces as well. (Type declarations versus a record parameter.)

[weaversa]

why is no operator required to "apply" the type variable declarations to the type?

Then you'd have an extra => between the variables and constraints.

encrypt :
    {k, m} =>
    fin k  =>  k >= m  =>  // two  `=>`s!
    String k -> String m -> String m
encrypt psk pt = ct
  where
    ct = (take`{m} psk) ^ pt

[yav]

Is there something to resolve here or shall we close this? Some potential tasks:

• Remove the curried =>. I am not sure that its existence is intentional, and the notation is potentially misleading, as the "curried" constraints are just another notation for the "uncurried" version.
• Maybe add some more documentation on the syntax of types. I'd assume the syntax is documented somewhere, but we should check that this is indeed the case, and if not we should add it.

[brianhuffman]

Its existence is most definitely intentional; the feature was requested in #599.

[yav]

Ah, good to know. Well, in that case, is there something that we need to do here?

[AssemblyZig]

If the consensus is that => functions as desired/intended, some enhanced documentation of its role would be useful. E.g., what is a descriptive English term or phrase for the => operator/functionality?

[jpziegler]

We've attempted an English-language breakdown of types in the Cryptol course we've been working on.

To check it out and see if you agree with our interpretation, search for "breakdown" here:

https://github.com/weaversa/cryptol-course/blob/master/labs/Language/Basics.md

[WeeknightMVP]

@AssemblyZig Cryptol supports type inference, e.g. [0,1,2]:[_]Integer. When you introduce a definition with type variables and a signature but no constraints, are you hoping for constraint inference, e.g. swap: {n, w, a} _ => [n]a -> w -> w -> [n]a (which Cryptol (EDIT: syntax) does not currently support)?

[atomb]

This seems to have converged in the need for a reference manual, which we now have a PR for: #1188

[atomb]

And there's a ticket for it now, as well: #1260