comments on the language reference

language-reference-comments.md

reviewing Unison's LanguageReference.md master@81b65b, i.e. this

Overall:

• This doc is awesome: nicely written, thorough, not trying to be too formal, nice use of examples.
• It needs a table of contents to give the reader an overview.

In ‘type signature’:

• say that Nat means natural number, and that that means whole numbers starting at zero
• ‘meets’->’matches’?

In ‘term definition’:

• ‘expression in the’ -> ‘expression on the’
• if you’re going to use drop n 1 instead of the n - 1 everyone would have expected, I think you need some explanation of why you’ve done it like this, or a forward reference to one

In ‘user-defined abilities’

• you used ‘data constructors’ but I think it must be some other term needed here? ‘request’?
• you pointedly call A an ‘ability type constructor’, but that’s a bit confusing here because its also an ability type, on account of having no type parameters. Would be cleared up by mentioning here that an ability declaration can also have type parameters. (I found myself wondering about that at this point, comparing with the preceding stuff about type declarations, so I think this would be a good addition.)

In ‘unison expressions’:

• ‘evaluated strictly from left to right’ – not clear whether ‘strictly’ is meant informally as emphasis of ‘left to right’, or whether you’re saying that left-to-right implies strictness, or whether ‘strictly’ is adding an extra piece of information here. If this is the bit where you’re introducing the fact that unison is strictly evaluated, then I think it deserves a bit more – just a sentence or two. ‘Note that arguments are evaluated (once) regardless of whether the function that receives them ends up using them’ or something. Ah, or give a forward reference to the section on function application.

In ‘identifiers’

• can operators start with a ., even despite the namespace qualification stuff?

In ‘blocks and statements’:

• worth mentioning that variable bindings can be preceded by a type signature? And that they can be functions with parameters? Also why are we calling them ‘variables’? It suggests they can be mutated. Maybe just say ‘binds the name x’.
• I think that statements, even apart from the final one, can just be expressions, right? I see that this is a special case of an action, but that won’t be obvious to people. I think this is worth mentioning, even though it can’t affect runtime behaviour to add an expression like this, because it improves the intuition for what blocks are about. (Also can be used to check an expression typechecks, or that an expression’s type matches some annotation.) So I’d maybe add to (2) the fact that an action with no abilities is just an expression, and that this is valid too.
• I think you should have a concrete example of a block with some statements in. This is the first section you haven’t had an example (apart from abilities, where I agree that makes sense.)

In ‘lexical syntax of blocks’:

• ‘Each statement in the block must be indented to line up with the left edge of the block’ – is it actually OK if it’s to the right of the left edge? i.e. can blocks slant inwards, If it’s allowed then I think it’s worth saying so here.
• Again, I think you should have some examples here. Layout is actually pretty hard to learn.

In ‘literals’:

• The ‘natural number or 64-bit unsigned integer’ bit is a surprising, for two reasons: (1) it sounded from the name like we were claiming that ‘natural number’ was the thing from math, and now it turns out that it’s fixed-width, and (2) I initially read ’or 64-bit unsigned integer’ as describing some other type than ‘natural number’ – I think you need to unpack this e.g. ‘a natural number, in other words, a 64-bit unsigned integer’. You introduced Nat already before – I think somewhere between here and there you need to give a forward ref to an explanation of whether we have arbitrary-precision integers, and whether anyone needs to worry about integer wrap.
  Opinion: I’m a bit worried about calling it Nat if it’s not arbitrary precision. It sounds initially like this is a language that means business about embodying mathematical semantics, and then it turns out we were just kidding. I think we should say something like, ‘in future, Unison will support arbitrary-precision arithmetic, exposed through the types Natural and Integer. The types with abbreviated names Nat and Int are 64-bit types, with two’s-complement wrapping behaviour.’ (or whatever)
• ‘A text literal of type .base.Text is any sequence of characters…’ really any? Any Unicode -character? Can the toolchain (including my editor) cope with literally any character?
• ‘Escape Sequences section’ add a hyperlink
• ‘A text literal can span multiple lines, and newlines do not terminate text literals.’ The text here leaves me with a question: Is a newline actually treated as part of the literal or is it assumed to be so I can wrap the literal in my editor and so deleted? And what if I do want to wrap the literal – is there syntax for that like with haskell’s slashes?
• typo ‘trough’ -> ‘through’
• ‘A unary tuple (a) is identical with the expression a.’ In the scheme for tuple types, unary tuples are of type Tuple a Unit, right? Is this accessible using the type language sugar (a)? Sounds like it’s not accessible using the term language sugar (a), if I read you right. I’m just a bit worried that this is an irregularity which is going to be annoying at some point in the future (maybe for generic programming or metaprogramming.)

In ‘comments’:

• maybe nod to the fact that unison doesn’t currently support block comments, since it will surprise everyone who reads this?

-- pause 1

In ‘type annotations’:

• edit-o: ‘This tells Unison that e is of type T (or a subtype of type T), and Unison will check that it does.’ -> ‘check that it is’; but doesn’t make sense – why does it need to check something that it’s been told? Rather ‘tells Unison that you believe e should match type T – the typechecker then checks that that’s true’ (or something)

In ‘function application:

• typo ‘isinfix’
• I had never seen the word ‘parenthese’ before – so I’d recommend ‘parentheses’.
• typo ‘paranthesizes’ -> ‘parenthesizes’
• You use the word ‘generally’ – does this mean ‘always’ or ‘mostly, apart from some exceptions we won’t go into’?
• ‘non-strict semantics’ -> ‘non-strict semantics – see the next section.’
• totally feel free to ignore this one, I’m sorry for mentioning it… but I’m finding ‘identical with’ distracting; ‘identical to’ is (apparently) about 4 times more common

In ‘quoted computations’:

• Are we really calling it ‘quoted’ rather than ‘delayed’? ‘Delayed’ gives the intuition better than ‘quoted’ I find. ‘Quoted’ encourages confusion with quoting in the metaprogramming sense. ‘Quoted’ doesn’t even seem right, because a quotation has quote marks at both ends. ‘force’ is a plausible opposite of ‘delay’, but not of ‘quote’.
• This section needs some examples and motivation. Why is quoting/delaying sufficiently important to get its own syntax?
• I think you should acknowledge the existence of expressions like ''foo etc.

In ‘case expressions’:

• not sure that the “Where e” sentence after the example quite works
• typo ‘subsituted’
• ‘Other patterns remain unevaluated’ Do you mean, other match bodies remain unevaluated?
• ‘If the pattern doesn’t match then the next pattern is tried and so on’ This reads like an explanation of the implementation. But I think pattern match compilation can be done in a way that doesn’t always need patterns to be tried in sequence? Maybe you mean ‘you can think of it as trying the patterns in sequence’ (or something). I just mention it because if people read it as an implementation statement, then they might think ‘that’s not a very good implementation…’

In ‘pattern matching’:

• ‘reduce to 42’ Not sure you’ve mentioned reduction so far. I think it’s quite a technical term. Up to now you’ve talked about evaluation – maybe stick to that?
• Your case 2 + 2 example has branches for 4 and 6 and nothing else – but you’ve just said it’s an error if none of the patterns match, hopefully in future a compile time error. Maybe add a blank pattern (and switch it so you introduce those first). Ditto several of your examples in this section.
• Blank patterns: your example here doesn’t seem to be an example of the thing being described. You describe things like _x, but then show _. And what’s the significance of the x, if it’s not used to bind a name?
• ‘List patterns’ – looks like formatting has gone screwy, not seeing each of the 3 numbered options on its own line. Same with ‘ability patterns’.
• typo ‘ablity’

-- pause 2 – end of patterns

-- switching to master@969972 i.e. this

In section ‘use clauses’:

• you say ‘the code after the use clause’, but I think(/hope) that it doesn’t apply after the end of the lexical scope in which it appears.

In section ‘hashes’:

• I think you should say briefly that a hash is calculated as a digest of the team/type’s internal structure, excluding names. And why that’s useful, as opposed to just calling things by their name. At the moment it’s like ‘and why are hashes a thing?’

In ‘literal hash references’:

• I’d put built-in references at the end of the list since the reader is unlikely to meet them much.

• Give an example: so #a5e828 or whatever rather than just #x. Even if it has to be 104 chars!

• (The example #abc123e you gave earlier under hash literals suggests that the literals use hex chars (0-9a-f) – maybe change that example if that’s not true?)

• In ‘short hashes’, it leaves me thinking, ‘how short hashes can I get away with giving; when do I have to start worrying about collisions’, and ‘how would unison handle it if I gave a short hash which was ambiguous due to a collision’? In ‘unison types’:

• Not sure, but I’d say it might actually be worth putting some examples in this top section showing some types in the context of code. So a term binding and its type declaration, and a term with a type ascription. As it is, going straight into ‘type variables’ which just shows some normal-looking names, it feels a bit like ‘what are we doing here again?’

• Maybe also try and briefly tackle what a type is and what a type is for! I know papers have been written about that question. Something about classifying values by their structure, and computations according to the values they produce?

In ‘universally quantified types’:

• I’d say make ‘Scoped Type Variables’ into a hyperlink.
• The last para is a bit confusing – if it has type ‘forall x. List x’, how can it also have type ‘List Int’? Maybe say the former is the principle type (?), and that latter is a type that conforms to it? (or whatever is in fact true…) Also possibly confusing: why are you writing List x instead of [x].

In ‘scoped type variables’:

• since you’re already talking about when identically named things are the same or not, I think you should refer to the fact that the x in the id x = x bit of your example is not referring to the same x as in the line above. Either that or choose a different letter. I remember this was a big source of confusion for me, so other readers might get stuck on this bit. (Also you just raised an issue proposing to ban the id 42 bit, so maybe add a temp =.)

In ‘type constructors’:

• Do you really want to give Tuple Nat Int as an example? I don’t think that would ever be produced by the tuple syntax, so there’s a sense in which it’s not a tuple, which is then confusing given the type constructor name. I’d switch to (Nat, Int) and refer to the fact this is using some sugar. Maybe we need an alias Pair for Tuple or maybe they should even be two unique types - I didn’t think of this back when you switched it. Certainly having to say Tuple when you mean Pair is confusing, since Pair is not actually a Tuple.
• In ‘kinds of types’, I think it needs a sentence on why you’re telling us this, mentioning the fact that the kind syntax you’re introducing does not appear in unison programs.

In ‘built-in types’:

• not sure what to do about the duplication between this section and the section on literals. Maybe nothing. Or maybe add an xref from this section to the literals section as a ‘for more detail see…’ The section on literals is a better take on ‘meet the basic unison types’.

In ‘built-in type constructors’:

• the stuff about tuples is duplicated from the ‘tuple types’ section – I’d replace with an xref.
• On .base.List, I’d mention the [] sugar here.

In ‘abilities and ability handlers’:

• In previous similar sections, you’ve used the word ‘formally’ to flag this kind of text, and also provided informal text too – I think that would be a good approach here also.
• I think you should have something at the top briefly on why this stuff is needed, and what the overall idea for effectful programming is. ‘Unison is a purely functional language, meaning that no expressions have any side effects. But we still need to be able to write programs that have side effects – writing to disk, doing network I/O, and so on. Ability types are Unison’s way of allowing a computation to describe a side effect it would like to have. Handlers then interpret that side effect, often by translating it in turn to a computation using the built-in {IO} ability. Unison has a built-in handler for the {IO} ability, and it is being executed using this handler that is in fact the only way for a Unison program to have a side effect.’ Or something!

In ‘abilities in function types’:

• Unison sometimes emits a funny Unicode e (is it 𝕖?) which will be a bit scary when people first see it. So maybe show an example here (or get rid of it…?)
• ‘Abilities are provided by handle blocks. Maybe also mention {IO}` being provided by the runtime for executing a top-level program.
• Maybe mention the fact that we think of the {A} in ->{A} as being attached to the arrow? And spell out how we should interpret `X ->{A} Y ->{B} Z’, since that’s quite hard to get your head around.

In ‘user-defined abilities’:

• You’ve called this Store rather than State - I think that’s OK as long as you’ve decided that Store is going to be the canonical name in the standard library and other docs. If there’s already a State in the base libs and you just want to avoid defining it here, then add a note to say that it exists and what its name is.
• You should make this section a tiny bit more tutorial. What does this Store example mean? Why might it be used?

In ‘ability handlers’:

• ‘A constructor {A} T for some ability A and some type T’I think {A} T is not actually a constructor, but rather the type of one? Or if not, then I am confused and could do with an example here instead.
• This section is pretty hard to understand. I think that’s probably inevitable, but you should acknowledge it by saying ‘The examples in the next section should help give a intuition for how this fits together.’

In ‘pattern matching on ability constructors’:

• I think you’re going to have to try and explain in this section what a continuation is. Can you talk about your p example and say what bit is the continuation for the call to Abort.aborting?
• You’ve called out the case where the continuation is discarded, so maybe mention that it can be called multiple times.
• I think this would be a good place to draw attention to the fact that aborting : () is not actually giving the type signature of aborting - it’s actually {Abort} (). (I do like that feature BTW.)
• I think you should add a type signature for p to the code sample, to help the reader confirm to themselves that the ability magic has been fully contained within p.
• You should mention what the first parameter to storeHandler is doing – it’s where the actual stored value lives, and that the changing value is captured by the changing values passed to each of the recursive calls to the handler.
• Say what the argument(s) to the continuation are.
• Worth saying something comforting here about this mutual recursion not blowing the stack?

In ‘name resolution and the environment’:

• The second para makes you ask: are types and terms in separate namespaces?

-- pause 3, first pass complete, might come back for another think

-- now on master@4a0fd, i.e. this

• Typos: search for ‘mofifyStore’, ‘must we well’, ‘will matches when’.
• Omissions?
  • Unique types
  • namespace
  • Universal.== etc
  • > watch expressions, maybe?
  • comment on lack of fixity?
  • ? (i.e. AskInfo)
• It would be interesting to see a list of things that can make a unison program crash. Does that belong here? Is it just incomplete pattern matches?
• A thought for later when we have lots of great tutorials: I think we should have some links to tutorials from the language reference. For example, if someone with no prior contact with abilities/effects finds themselves reading the abilities section of the language reference, they’d probably be better served by switching to a more long-form tutorial that takes it slower.
• What about some coverage of what information from a term actually gets fed into its hash digest? Or maybe that’s not observable at the language level, only when trying to add things to the codebase.
• Is there anything to say about the memory model, garbage collection?
• Anything about how to actually run a program, what a ‘main()’ function looks like, what can be passed to execute in the CLI? Maybe out of scope.
• (Maybe there should be a link to library documentation for IO, when we have some.)

-- end! 😊