AST-47 List functions in AS, inspired by SML Basis library

[matthewhammer]

(This is a cleaner version of PR #128)

[matthewhammer]

@crusso @rossberg @nomeata
Is there a reason that each AssertE expression types as T.unit and not T.Any?

That decision seems to make the function above, from the SML Basis, impossible to type in AS. While this function may not be a great design for AS, due to the lack of exception handling, it still seems useful (and practical for many dev workflows) for a program to fail dynamically while it statically inhabits any type.

[matthewhammer]

Update: Talked to Claudio on Slack about this; will file an issue shortly.

[rossberg]

Not sure how Any would help, that's the top type, so only compatible with itself. You probably meant None, the bottom type, but a function cannot have that type and ever return.

We probably should have an unreachable expression.

[matthewhammer]

Right; Claudio clarified elsewhere (on Slack) that we'd want None and not Any here.

OK.

[paulyoung]

I think I've encountered this before and worked around it. Will try to find an example.

[paulyoung]

Not sure if it's the same issue, but here I was expecting the return type of the lambda to be () and had to ascribe (())

https://github.com/dfinity-lab/dev/blob/032c02665f237de9655e238415bf3b0d3d666b87/experimental/actorspec/src/List.as#L79-L83

func traverse_<A>(f : A -> (), xs : List<A>) {
  foldl<A, ()>(func (_ : (), x : A) : (()) {
    f(x);
  }, (), xs);
};

[matthewhammer]

Ah, interesting. Thanks!

BTW: Do you know if there's an existing issue (did you make one?); if not, I'll make a new one.

[paulyoung]

I couldn't find one so I assume that I forgot.

[rossberg]

That's working as intended. We have n-ary parameters and results and first-class tuples, but they are not the same thing, even though they are coerced implicitly. But still, (T,U) -> (T,U) is a different type from ((T,U)) -> ((T,U)) (mainly because the coercion isn't possible in the polymorphic case).

[matthewhammer]

Hmm.. I see. Thanks for that explanation. I was able to fix the code to avoid this error.

Aside (not critical)

This "n-ary result" design does not match my mental "notional machine" very well, which is based on CBPV. In CBPV, I make sense of n-ary arguments as being CBPV "currying". Like the functions here, "ordinary currying" in CBPV does not permit partial application.

However, CBPV is asymmetric: Although functions generally take many inputs, each sub-computation has one result. Categorically, I think opetopes have the same structure (zero or more inputs, and one output), though I don't know category theory very well.

Having said all that, I'll try to evolve my mental model now ;)

[rossberg]

Oh, I absolutely agree with you. It would be great if we didn't need to make this distinction. Unfortunately, there is no efficient way to implement it such that it works with type abstraction if you want to raise function arity in the implementation. (That has been a long pain point of many functional languages. See e.g. Ocaml's treatment of datatype constructors -- same thing.)

[matthewhammer]

Interesting. Yes, pragmatism seems to be at odds with the "nice"/"clean" design, as usual.

FWIW, I interpret data constructors in CBPV as being sugar for value types, and never standing in for computation type arrows, except if they get "promoted" (eta expanded) by a "real" lambda. That agrees with my (limited) understanding of OCaml constructors vs OCaml functions, but I may be wrong.

[rossberg]

I'd be less penurious and name these head and tail.

But to be honest, I wonder how useful these are without exceptions. Matching on the list itself is less verbose than matching on the option.

[matthewhammer]

OK, sounds fine to me.

(In general, I have no desire to choose the names of library functions. I have no real preferences, and mostly just want to be told what naming conventions to follow. That goes for all of the naming nitpicks lower down, too. I tried to follow the SML conventions where they made sense, though I now see that I deviated in some places; it wasn't very intentional.)

[rossberg]

How about using a record {head, tail}, which would be nicer esp for pattern matching? Currently, records are a bit annoying because you have to write new, but I have some sugar in mind for allowing to omit that.

[nomeata]

One argument for tuples would be that it is less efficient (records need more memory and more time to look up fields because of polymorphism). Of course, programmer ergonomics often trump run-time efficiency, but it is a pity that we can’t have both.

[rossberg]

Yeah, you're probably right. Some day somebody will propose "final" object types. :)

[matthewhammer]

I don't see how records, with their heavier syntax, are "nicer" for matching a pair.

Am I missing something?

[rossberg]

Well, let's say more self documenting. Also, we should probably allow label punning in patterns, as most other langs.

[matthewhammer]

OK, I anticipate hating the version of this file (list.as) where all the patterns on the LHS take 2 or 3 times their current length, but I'm certainly willing to try it, to find out.

[crusso]

Note we don't have record patterns yet.

[matthewhammer]

Haha, Ok. Thanks for that note.

[rossberg]

Hah, excellent point. I don't even remember why why.

Anyway, in that case, keeping it a pair is probably better for now. Sorry for the noise.

[rossberg]

Not sure how Any would help, that's the top type, so only compatible with itself. You probably meant None, the bottom type, but a function cannot have that type and ever return.

We probably should have an unreachable expression.

[rossberg]

If we really want to have these functions then we should at least decide for one version. I'd prefer the optional one.

[matthewhammer]

Yep, OK.

I had both because until you fixed the type checker bug, only one worked (viz., the "stranger" one that uses tlo, which we can drop now).

[crusso]

Could we allow question marks in identifiers? The tl and tl? would be nice variations... alternatively try_tl rather than tlo ?

[matthewhammer]

Interesting idea.

In this case, I just dropped the versions that raise exceptions (per @rossberg's comment), so there's no need to have two different names, at least not here.

Do we anticipate other situations where we need two versions for the same operation (fail-via-exception vs optional return)? Don't we just always just prefer options in those cases?

[rossberg]

Allowing question marks in ids would require using spaces for the option type, though (? Nat etc). Maybe not a big problem, but I could see that as a very frequent source of surprise and confusion.

And Schemers would probably object to using f? for something else then predicates. :)

[rossberg]

Same as above, I think we should only have one version.

[matthewhammer]

OK. I'll prefer the versions that use optional returns, as discussed elsewhere.

[rossberg]

Thunk? Why the record?

[matthewhammer]

I don't have a strong feeling here, but I prefer to write t.force() and not t ().

The latter form is more concise, but it also makes the forces in the code harder to locate; so I don't see it as a real benefit. I like these operations to be very explicit, for inspecting the "laziness" of each purportedly lazy algorithm by just looking for the word "force".

[rossberg]

I think I'm not sure what you intend this for. Is it even worth introducing a name for this? Don't know that any other library would have it. The name force would rather suggest a lazy suspension, but then you need a different type.

[rossberg]

You want to allow empty streams, so it must be the latter. I'd define

type Stream<T> = ?{head : T; next : () -> Stream<T>}

[matthewhammer]

Ok, that def sounds fine to me, but why not just use a pair?

(What's the advantage of using records for pairs? Just readability, or something more?)

[crusso]

I'm beginning to sense we might want to add non-extensible records for documentation and efficiency.
I expect the same thing will happen for variants so we can do efficient jump tables...

[rossberg]

Why not simply Thunk<T> = () -> T?

[matthewhammer]

Haha. What is your convention for preferring records with named fields vs no records and no named fields?

• Pairs should be records
• Unpaired functions should be just functions

?

[rossberg]

That's working as intended. We have n-ary parameters and results and first-class tuples, but they are not the same thing, even though they are coerced implicitly. But still, (T,U) -> (T,U) is a different type from ((T,U)) -> ((T,U)) (mainly because the coercion isn't possible in the polymorphic case).

[rossberg]

Not sure I get what this is for. Seems less convenient then a literal pair.

[matthewhammer]

Laziness. A thunk producing a pair is not the same as a pair of thunks.

[rossberg]

Oh, I see, I missed the thunkification of the result.

Is this worth having? It seems very specialised. I'd suggest not making the lib too sweeping for now.

[matthewhammer]

Sure, this thunk module can be dropped. It's more of an experiment of me using actorscript than a useful module for others.

OTOH, streams, or other lazy structures (beyond mere thunks) may be more useful.

[matthewhammer]

As everyone may or may not be aware, the compiler's front end steps (lexer and parser) do not recognize words, or even the types for words. Ultimately, when these concepts are supported, we want to use them for hashes and short (word sized) bit strings.

Until then, I'm using linked lists of booleans.

[crusso]

I'm a little confused. The interpreter does support words, it's just the compiler that doesn't yet.

[matthewhammer]

Yes. I should have looked in prelude.ml more carefully.