Mentions légales du service

Skip to content
Snippets Groups Projects

New System F constructs

Merged MARTINOT Olivier requested to merge omartino/inferno:new-f-constructs into master

Add new System F constructs (variants, records, pattern-matching) with corresponding printer and type checker modifications. (cc @gasche)

Edited by MARTINOT Olivier

Merge request reports

Merged by POTTIER FrancoisPOTTIER Francois 4 years ago (Dec 2, 2020 3:39pm UTC)

Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • MARTINOT Olivier changed title from New f constructs to New System F constructs

    changed title from New f constructs to New System F constructs

  • MARTINOT Olivier changed the description

    changed the description

  • 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.)

  • SCHERER Gabriel mentioned in merge request !10 (closed)

    mentioned in merge request !10 (closed)

  • MARTINOT Olivier added 57 commits

    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

    Compare with previous version

  • MARTINOT Olivier added 59 commits

    added 59 commits

    Compare with previous version

  • mentioned in commit 97ad7bf6

Please register or sign in to reply
Loading