New System F constructs
Add new System F constructs (variants, records, pattern-matching) with corresponding printer and type checker modifications. (cc @gasche)
Merge request reports
Activity
Note: the "variants" in System F are really structural types (structural n-ary sums, just like its structural n-ary products). In particular, inference for ML variants (coming in a later PR) translates from nominal ML types to structural F types. We considered using "named" sums and products in System F, but for now they are just used by-position with an index, as in standard simply-typed presentations.
(One could also decide to not have sums in System F and instead use the usual impredicative encodings, but our understanding of the current Client philosophy is that the term-level constructs should remain essentially unchanged between ML and F, and an impredicative translation would not preserve this property. In our current prototype the translation of types is simple but non-trivial, and the translation on terms is obvious.)
mentioned in merge request !10 (closed)
added 57 commits
- a3840b76 - separate tests
- dcb6df34 - Nominal2Debruijn.concat : env -> env -> env
- a1cb15c7 - Merge pull request 'Nominal2Debruijn.concat : env -> env -> env' (#1 (closed)) from...
- 27e824b8 - Cleaner version of two separate test files
- 70d02b45 - Merge pull request 'separate tests' (#2 (closed)) from separate-test into master
- 66628474 - rename client/Client into client/Infer to name the library Client
- 819fd28f - separate tests further into a test/ directory
- 4e4f4115 - Merge pull request 'Separate tests further' (#4 (closed)) from...
- a512cb60 - add product and sum type in System F
- f6b6b61d - add match construct in system F
- 68d98d2a - Use type environment concatenation in F type checker, add test
- 4f9652e1 - Improve FPrinter
- fa5e4674 - Improve FTypeChecker (error handling, code factorization)
- 2a5daa81 - Add type annotation in pattern-matching
- 9f77b1df - Fix bug in FTypeChecker interface
- b9b2a5b6 - Environment variable must now be set to enable random tests
- 33f84480 - Fix a typo
- d857bd6a - Add pattern-matching example
- aec8a1a7 - Fix bug in printer
- 42c35546 - Simplify spaghetti code
- 29f2903c - Changes in type annotations of injections (list of tyeps instead of sum type)
- 7a2ebdd7 - Better error handling : type errors are now all part of the same sum type
- adac72c7 - Print tuple unambiguously
- 0028456e - Fix error handling in FTypeChecker
- bbd47885 - Auxiliary function moved in a more appropriate place
- a7921a6d - More readable type variable names in hand written tests
- d588ba83 - Rename union to concat, concat_disjoint returns a result
- da874d03 - Rebase with master
- b4445ceb - Merge pull request 'new-f-constructs' (#3 (closed)) from new-f-constructs into master
- 1ccc3430 - [minor] Fprinter: move the print-term helpers before the recursive block
- dbb9e76e - FPrinter: fix print_tuple
- c45c70bb - fix bound checking in nth_type
- 021f6ead - even when INFERNO_SLOW_TESTS is not test, do some *quick* random testing
- c25014e2 - Merge pull request 'fix-nth_type-bound-checking' (#7) from...
- 835ef283 - Merge pull request 'FPrinter: fix `print_tuple`' (#6) from...
- 455fd161 - restore the System F tests that were disabled by #4 (closed)
- 4f5d8dba - [minor] typo in TestF.ml
- 7718ec79 - Merge pull request 'restore the System F tests that were disabled by #4 (closed)' (#5)...
- 62f62c23 - F: add a LetProd construct
- b7d5bdf4 - LetProd: Fail more gracefully when there is an arity mismatch
- a893f86d - ML: remove Proj, which does not extend to n-ary products
- dc530b64 - Infer: use n-ary product structures
- de498f2b - ML: LetProd, with type inference in CPS
- c527ded7 - Infer: make Tuple a n-ary construct
- ad3cafd0 - Merge pull request 'N-ary tuples in ML, to reveal the difficulty of creating...
- f6d439c9 - Pretty print types without levels
- d2c20433 - Pretty print terms without levels
- 34f850c8 - Use print_term_*/print_type_* instead of *
- 07555333 - Proj/Inj on their own level
- 8103dacf - Move already delimited cases into atom
- bc7b3895 - List unhandled constructors in the atom case
- cf68a69b - In the Let/LetProd cases, we now call print_term instead of print_term_abs
- 66e2905e - In App/TyApp cases, we now call print_term_app instead of print_term_atom
- 81ab70ff - PInj has now its own level
- 1a142aa7 - Change levels for subterms of Let/LetProd/App
- 682e7c00 - Fix typo
- 097378a9 - Merge pull request 'pretty-printer' (#9) from pretty-printer into master
Toggle commit listadded 59 commits
Toggle commit listmentioned in commit 97ad7bf6