This is awesome, and a big step forward for OCaml. Only criticism is that it seems difficult/awkward that you need different functions/values for each phase. In other staged macro systems (Scala/LMS, Rust/Compiler Plugins) you can refer to the same functions in any phase, and you can also splice values from the staging phase into the runtime phase without explicit use of a function like Expr.of_int.
There are some difficulties with moving arbitrary values between phases: it's easy to move an int or a list, but what about a mutable reference or a closure?
However, I don't think this will ultimately be a problem in practice, for two reasons. First, global values can be used in different phases via "module lifting". Second, there's a separate proposal for adding overloading to OCaml in the form of modular implicits:
Modular implicits will make it possible to use a single overload function ('lift', say) in place of a family of functions 'Expr.of_int', 'Expr.of_float', etc., which will make things much less awkward. And it's only a small step from there to having 'lift' called implicitly/automatically at appropriate points. Here's a message from an earlier discussion with a few more details:
> There are some difficulties with moving arbitrary values between phases: it's easy to move an int or a list, but what about a mutable reference or a closure?
Wasn't this already answered by "Closing the Stage" [1]?
"Closing the Stage" is about a different interaction between staging and closures: that (with some care) staging constructs can be elaborated into closures in an unstaged calculus.
The problem with moving arbitrary values between phases with macros is that values can refer to bits of the runtime environment that cease to exist when compilation is finished.
> that (with some care) staging constructs can be elaborated into closures in an unstaged calculus.
Exactly, which seems to provide the necessary semantics for references that you mentioned. Clarifying staging semantics for difficult abstractions like refs by elaboration into well understood closure semantics was the point of the paper.
This sounds very handy and I definitely need to learn more about LMS and Compiler Plugins. I wonder then what are the limitations on the values you can pass automatically across phases, since there must be (you cannot transfer e.g. a file handle from compile-time to run-time).
As far as I understand, for LMS: Those types T for which one has implemented needed operations for the Rep[T] type.
Shameless plug: For another comparison of MetaOCaml, LMS, Terra and AnyDSL (our approach) under the lens of staging/partial evaluation see our paper from GPCE'15: http://www.cdl.uni-saarland.de/papers/gpce15.pdf
I work on lms and we are preparing a new version where Rep is implemented as a typeclass instead of a monad. It's much more pleasant because you manipulate IR.Int and scala.Int. So with the proper import you actually handle IR.Int so you're staged code is no different than a normal code.
I also agree that there seems to be too much separation between the phases. I wonder if this is a design choice or a design limitation. MetaOCaml also requires explicit lifting/unlifting of values.
There are certainly some design choices here. I want to emphasize that in the few projects where I've used macros (e.g. https://github.com/OlivierNicole/macros-examples), I found that these translating functions were scarcely needed and I never had to pass a non-standard type between phases.
Can someone tell me why I would want statically typed macros? Why not just simply type check after macro expansion phase? Seems a lot simpler and more intuitive.
It strongly feels like a case of everything looks like a nail when you really like hammers (static typing), but I am willing to be proven wrong.
There may be a bunch of other reasons, but the one that springs to mind is localisation of errors. You'd ideally like to know about any mistakes you've made in your macro before you run your macro. And when you do learn about a mistake you'd like the error to describe where the mistake is in macro-land rather than generated-code land.
I agree, you may wish to do that but I was answering the question "What is the utility of typed-templates", not "contrast type and runtime error tradeoffs".
Firstly, if your macro does not typecheck, it means that executing it might result in a segfault or something similar, since macros are regular OCaml functions.
Secondly, if macro typechecks, then it is guaranteed to expand without errors, and I think that's a nice guarantee to have.
> Firstly, if your macro does not typecheck, it means that executing it might result in a segfault or something similar, since macros are regular OCaml functions.
I see. The only time I've extensively used (real) macros has been with racket, where they aren't regular functions at all. I suppose my ignorance of Ocaml macros is showing here.
Oh I see what you mean. For now, we have made the choice to compile static code to OCaml bytecode, whatever the compilation target is. While this enables the use of macros regardless of the target (e.g. it works in `ocamlopt`, the native compiler), it does make it necessary to compile a module to bytecode if you want to lift it. It's not a big deal with an adapted build system, but a distant future we might support native compilation of macros on some architectures.
Having never tried OCaml, what advantages does it have over other languages? Two languages I don't know seem more interesting, Clojure and Rust. Generally I work in Swift these days.
IMO, the single most interesting thing about OCaml is its object model. On one hand, you have a fairly conventional setup with classes, methods, inheritance, generics etc. On the other hand, the entire system is structurally typed, with pervasive type inference. Recycling bits from my earlier comment on the subject...
# let f obj x y = (obj#m x)#n y;;
val f : < m : 'a -> < n : 'b -> 'c; .. >; .. > -> 'a -> 'b -> 'c = <fun>
Here I defined a function taking 3 arguments, called method m on obj, passing x as argument, then called method n on the result of that, passing y as argument.
Note the inferred type signature for this: the first argument is of type <m : 'a -> <n : 'b -> 'c; ..>; ..> - i.e. any object that has a method named m (and possibly some other unspecified members - that's what ".." means), with said method m having a signature that allows us to pass some 'a, and returning another object of type <n : 'b -> 'c; ..> - i.e. something with a method named n that accepts 'b and returns 'c. 'a and 'b' are then used as types of x and y, respectively, and 'c is the the result of f.
This is actually row polymorphism rather than structural subtyping. The difference is rather small, but important:
Under structural subtyping (or any kind of subtyping, for that matter), the subtyping relation admits a rule called "subsumption", which can lead to information loss. Consider this behavior, under structural subtyping:
fun f {x : real, y : real} = {x = 2 * x, y = 2 * y};
(* f : {x : real, y : real} -> {x : real, y : real} *)
f {x = 2.0, y = 3.0, z = 4.0};
(* it = {x = 4.0, y = 6.0}; *)
Above, when `f` is applied to a subrecord with an additional `z : real` field, the result is missing the extra field! This is because the subrecord was subsumed by the (super-) record type taken by `f`, leading to information loss. This is the reason why you often see people using up-casts in languages like Java (especially before generics were introduced) and Go (which is lacking generics for some befuddling reason): up-casts allow you to circumvent the type system and force a particular value to take a particular type, thus recovering the lost information, but can be unsafe.
Under row polymorphism, however, you can achieve basically the same effect, but you get to save any unused/irrelevant type information inside of a row variable (the `..` in your example) and include it in the result. Then, no information is lost, and no safety is compromised:
fun f {x : real, y : real, R} = {x = 2 * x, y = 2 * y, R};
(* f : {x : real, y : real, _ : ..a} -> {x : real, y : real, _ : ..a} *)
f {x = 2.0, y = 3.0, z = 4.0};
(* it = {x = 4.0, y = 6.0, z = 4.0}; *)
Users of languages like Lua or Python might be reminded of "duck typing", and not without reason: row polymorphism enables many of the same programming patterns/techniques/abstractions in typed languages that are enabled by duck "typing" in untyped ones. It's a shame that more typed languages don't incorporate the idea, because it's a really wonderful one, and it can lighten the relative "burden" of writing typed code in some cases :)
The folks at INRIA has come up with some really neat stuff, and, if you haven't already, it's definitely worth it to check out their publications, too!
And, indeed, "static duck typing" is exactly what I'm thinking about when I'm dealing with OCaml objects.
FWIW, while it was relatively obscure, TypeScript is currently popularizing this concept (albeit with a lot less type inference). Although they also refer to it as "structural subtyping":
But if I understand correctly, they're basically doing the same thing that's going on here - the only difference is that the ".." is implicit in any TS interface type. Or am I wrong?
No problem! The difference between the two was something I personally struggled with at first, so now I feel like I've got a pretty good grasp on it. Funny how that works ;)
I don't see anything here in the TypeScript docs that looks like row polymorphism. Without a row variable somewhere in the type (even if it's inferred), I'm not sure it could be considered row polymorphism. However, they could be doing something fancy with their notion of type compatibility that avoids information loss without introducing row variables (which, I think, would similarly imply a lack of subsumption[0], and might not be sound, but the docs admit the system is unsound in places). It's also possible that every record type in TS carries an implicit row variable.
The important part is the (lack of) information loss, and good way to tell would be to construct a test case like the one I wrote above and see if you wind up losing your `z` field (information loss => subsumption => "by-the-book" subtyping).
This all reminds me that I've been meaning to spend some time with TypeScript :)
[0]: I've known type theorists who claim that without subsumption, there is no subtyping. I disagree because I think the fundamental/important part of subtyping is the subtyping relation itself.
I actually didn't fully understand your example originally (I missed the part where ".." now has a name!). I grok it now, and yeah, TS doesn't have it - there's simply no type-safe way to write a function like that (of course, TS being a strict superset of JS, you can still write it, it just won't typecheck).
It appears that this was discussed in the context of supporting the ES7 "spread" operator, since row variable is the obvious typed counterpart to that:
Ah! Good to know :) TypeScript seems like a neat language, and I've got a JavaScript project coming up so I intend to look into it more deeply soon.
Yeah, in my example, `R` is the row variable itself, and it represents all those other, irrelevant values in the record, while I gave it the name `_` in the type itself, since rows themselves don't have field labels, but rather represent sets of labels. In ML, the labels of the fields are part of the type, but the labels of the rows are not part of the type. Then, `..a` is a type variable representing the type of the row (it gets a distinct name because you can imagine a function which takes two separate records with two separate rows[0], or even a function which takes two records but constrains them to the same type with a single row[1]), and is akin to a type variable used for parametric polymorphism, such as `'a`, and, in Standard ML with eqtypes, `''a`.
To the best of my knowledge, the term "row" comes from The Definition of Standard ML, where the grammar given for the core language includes productions called "TyRow", "PatRow", and "ExpRow", which correspond to the syntax of record types, patterns, and expressions, respectively, but only the part in between the `{` and `}`:
(The `At` prefix means "atomic", and has a specific meaning in the definition.)
So, then, a row variable is one which literally holds a sequence of label×type or label×value pairs. It sometimes even feels like it's a metavariable which holds a branch of the syntax tree the way a variable in a macro does, which might be another reason why row polymorphism feels so cool ;)
Sorry if I'm boring you at this point, I just find this stuff really fascinating and fun :)
———
[0]: Any two records of any two record types, as long as they each have both an `x : real` and a `y : real`, with intentional information loss:
f : {x : real, y : real, ..a} -> {x : real, y : real, ..b} -> {x : real, y : real}
(* f {x = 1.0, y = 1.2, z = 1.3} {x = 1.0, y = 2.0, w = 42}; *)
(* ^ typechecks okay!
* row type `..a` can be different from row type `..b`,
* no problem
*)
[1]: Any two records which both have the same type, which can be any record type that at least has an `x : real` and a `y : real`:
f : {x : real, y : real, ..a} -> {x : real, y : real, ..a} -> {x : real, y : real, ..a}
(* f {x = 1.0, y = 1.2, z = 1.3} {x = 1.0, y = 2.0, z = 0.0}; *)
(* ^ typechecks okay! *)
(* f {x = 1.0, y = 1.2, z = 1.3} {x = 1.0, y = 2.0, w = 42}; *)
(* ^ type error!
* the second record has a different type than the first,
* but the type of `f` demands that they be the same type,
* since the single row `..a` must match itself
*)
A largely unrelated question: do you know why most ML dialects have this weird scoping rule for record members, where they share the same scope as the record itself (and so another record cannot easily reuse the same field name)? It seems awfully inconvenient, and it feels like it could be trivially resolved by allowing reuse with an explicit disambiguation syntax. Or am I missing something?
Which dialects? Both Standard ML and OCaml can handle multiple record types with homonymous fields just fine:
$ poly
Poly/ML 5.5.2 Release
> type point2 = {x : real, y : real};
type point2 = {x: real, y: real}
> type point3 = {x : real, y : real, z : real};
type point3 = {x: real, y: real, z: real}
> let val pt = {x = 1.0, y = 2.0} in #x pt end;
val it = 1.0: real
> let val pt = {x = 3.0, y = 4.0, z = 5.0} in #x pt end;
val it = 3.0: real
>
$ ocaml
OCaml version 4.03.0
# type point2 = {x : float; y : float};;
type point2 = { x : float; y : float; }
# type point3 = {x : float; y : float; z : float};;
type point3 = { x : float; y : float; z : float; }
# let pt = {x = 1.0; y = 2.0} in pt.x;;
- : float = 1.
# let pt = {x = 3.0; y = 4.0; z = 5.0} in pt.x;;
- : float = 3.
#
The only nuance with record labels in ML, as far as I can remember, is that the type of projection operations can be ambiguous if the exact type of the record is unknown (e.g., in `(fn pt => #x pt)`, the type of `pt` cannot be inferred since it could be `point2`, `point3`, `{x : int}`, `{x : real}`, ...; but this can be disambiguated with a type annotation: `(fn (pt : point3) => #x pt)`).
Perhaps I've misunderstood the question. If so, can you give me an example?
This is weird. Last time I really did anything with ML was ages ago, and I distinctly remember fighting with the fields... I wish I could remember the context, though.
Anyway, good to know that it's definitely not OCaml!
Over other languages in general? That's hard to say about any language :)
OCaml is a language in the ML family, is backed by INRIA and is the main language of Jane Street Capital (so it definitely has "real world" use!), which also contribute a lot to it. OCaml is pretty good for functional programming, and unlike Clojure, it's statically typed. If you like static typing -- which I personally think is the way to go -- that's a huge reason to prefer it over Clojure. You may also check out Haskell if you go that way.
An interesting case study about going to OCaml from another language (Python, in this case) was posted to HN many times already: http://roscidus.com/blog/blog/2014/06/06/python-to-ocaml-ret.... I recommend you read it if you want to learn more about why would one choose this language.
Why not choose a language in the ML family? Well, if not having C-like syntax is a deal breaker for you, then OCaml is going to frustrate you. A real programmer shouldn't let syntax stop them from learning new languages, though :)
Ultimately one has to try doing something with this kind of language, even if it's just a toy project. Just reading about it won't enlighten you much, and you will end up focusing on its syntax instead and deciding it looks too unfamiliar.
> Well, if not having C-like syntax is a deal breaker for you, then OCaml is going to frustrate you.
There is a new alternative Reason syntax (https://facebook.github.io/reason/mlCompared.html) which replaces some of the unusual syntax with braces and semicolons. Though it still probably looks less C-like than Swift. And I haven't tried writing anything in it, so can't say for sure if it really feels less weird than standard syntax on a "real program".
Oh, and the other neat thing is that OCaml cleanly separates subtyping and inheritance. In other words, in OCaml, class inheritance is for implementation reuse only, and is completely orthogonal to subtyping. In many common cases (similar to Java etc) inheritance does produce a subtyping relationship in practice; but because of this decoupling, you don't get one shoehorned onto your classes when you just want the other.
Ocaml is concise yet comparatively simple (despite various warts), offers good javascript interop and (quickly!) compiles to fast code and has a good type system. It's extensively used for language prototyping and tooling (e.g. at facebook). Rust's compiler was originally written in Ocaml: https://github.com/rust-lang/rust/tree/ef75860a0a72f79f97216....
Compared to Rust it compiles much faster, offers an interactive shell and is more expressive and mature, but doesn't offer similar low-level and parallelism capabilities and eco-system coherence (e.g. there are half a dozen competing build systems). I also believe that Rust, with it's clearly defined niche will win a much bigger total market share.
Compared to Clojure it offers static typing, much better startup times and native code compilation, but doesn't have similarly modern functional datatypes and the standard library is less well thought out.
There are a couple of other things which are rare or nonexistent in other languages:
- Polymorphic variants, the article linked downthread has some use cases
- a structurally typed OO system, as someone has already mentioned
It also has a few interesting syntactic ideas that I wish more languages would steal:
- Nice sugar for passing keyword arguments: `f ~somearg` is the same as `f ~some_arg: some_arg`. I wish I could do `f(=somearg, y)` instead of `f(somearg=somearg, y)` in python
- It supports new user-defined operators in a way that doesn't render your code unreadable, because the precedence is derived from existing operators.
- A nice syntax for "importing" from a namespace for an expression. Assuming Mod defines `foo` and you can write Mod.(foo x (bar f x)) instead of `Mod.foo x (Mod.bar f x)`
Honestly for me, it's just that it's damn useful. It's not especially new and shiny and hip, but it's easy to think in and easy to reason about. OCaml is a nice tool for writing software. That's about it. It's pretty simple functional programming that can switch to imperative and object-oriented programming where appropriate.
Love the design! Maybe not the simplest to use, and fairly verbose at times... but it's very clear what's going on at any given point - and given how hairy macros can get in production code, I think emphasizing clarity is the right approach.
What's the story for error messages? I read it's inspired by racket; the big thing about racket is that from what I hear it seems to be the only language that has good support for syntactic extension without sacrificing error reporting.
Let's take your static printf as a concrete example. Here's what a not so great error message looks like (ocaml's built in Printf):
utop # Printf.sprintf "Some int: %d another int: %d" 1 "2";;
Error: This expression has type string but an expression was expected of type int
Here's what a good error message looks like:
clang -Wall printf.c
printf.c:6:52: warning: format specifies type 'int' but the argument has type 'char *' [-Wformat]
printf ("Some int: %d some other int: %d\n", 1, "2");
~~ ^~~
%s
Notice how it also highlights the mismatched part in the string-based DSL.
The second message is arguably clearer, but I don't think anyone would be really hindered by the first one, especially given that, unlike in C, application of printf have an explicit type:
# Printf.sprintf "some int: %d another int: %d";;
- : int -> int -> string = <fun>
I think a general tendency in statically typed languages is that we like to write stuff using only the type system, rather than adding code to the compiler. Same for macros: we will rather have them proved correct by the typechecker than make them raise errors (also it is possible, through exceptions).
But maybe this is detrimental to clarity of errors in some cases. I'd be interested to see how Racket handles errors.
By contrast, common lisp and to a lesser extend clojure are also flexible but produce pretty bad error messages (and both have a culture that strongly de-prioritises approachability). This comes at a real productivity cost that doesn't disappear completely even with experience.
In lisp you can write a nice SQL like language or a math DSL without resorting to string parsing. In ocaml you kinda can't because the base syntax isn't that flexible. So I'd expect the problem to be worse and I don't think types are a magic fix. The worst and most voluble compiler error output known to man must be C++ template metaprograming errors.
