-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add records to the Inferno language (#103)
This PR brings records to the Inferno language. ### Syntax: ```ocaml let r1 = {ht = 1.51; wt = 62.4} in let bmi = fun r -> r.wt / (r.ht * r.ht) in bmi r1 ``` ### Types: A general record type looks like `{f1: t1; ...; fN: tN; 𝜌}` where 𝜌 is a type variable called a *row variable* representing either: - `⏊`: a special symbol denoting no further fields in the record, or - one or more fields with types `f1': t1'; ...; fN': tN'` The example above has the following types: ```ocaml r1 : {ht: double; wt: double} bmi : forall 'a. {ht: double; wt: double; 'a} -> double ``` Here, the concrete record `r1` has type `{ht: double; wt: double}` (which is syntactic sugar for `{ht: double; wt: double; ⏊}`, the record having exactly two fields), and the type of the function `bmi` uses a row variable `'a` denotes the fact that it accepts as argument any record that has at least the fields `ht` and `wt`. ### Differences to OCaml's Immediate Objects The description above is very similar to OCaml's ad-hoc objects, except that we retain the row variables in the types and show it to the user. The example above in OCaml would have the types: ```ocaml r1 : {ht: double; wt: double} bmi : {ht: double; wt: double; ...} -> double ``` I decided to keep the row variables explicit for now, because it makes the quantification on the "rest of the record fields" more explicit when we manually annotate functions. We can always change the pretty-printer and parser later to be like OCaml and hide row variables using the `...` syntax, if we prefer. --------- Co-authored-by: Daniel Casanueva <[email protected]>
- Loading branch information
1 parent
bebd4b4
commit c180370
Showing
24 changed files
with
6,581 additions
and
87 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.