Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Linear types #111

Merged
merged 78 commits into from Apr 13, 2020
Merged

Linear types #111

Changes from 75 commits
Commits
Show all changes
78 commits
Select commit Hold shift + click to select a range
35b7337
Linear types proposal (version 1)
facundominguez Nov 9, 2017
0443c3e
Linear types proposal (version 2)
aspiwack Nov 24, 2017
0a96720
Update PR number
aspiwack Feb 13, 2018
1ddaa64
Avoid number the main title
aspiwack Mar 9, 2018
6ab6b30
Typo
aspiwack Mar 9, 2018
d8788c7
Fix typos
aspiwack Mar 9, 2018
ceb3d05
Mention the unlifted data types proposal
aspiwack Mar 9, 2018
ca5d3d5
Alternatives: a section an unboxed data types
aspiwack Mar 9, 2018
fe68d3b
Fixe typos
aspiwack Mar 9, 2018
aed13ac
Clarify the point in the intro about optimisation passes
aspiwack Mar 9, 2018
d2210fc
Clarify that the Core Linter is modified to check linearity
aspiwack Mar 9, 2018
a85811c
Bad indentation leading to ill-rendered section
aspiwack Mar 9, 2018
92d65b0
Small typo
aspiwack Mar 9, 2018
2757cc1
Annotated binders, mixed-multiplicity records and record patterns
aspiwack Mar 9, 2018
bea28ca
Consistency
aspiwack Mar 9, 2018
9667411
Fix a link
aspiwack Mar 23, 2018
336b84f
Fix anchors
aspiwack Mar 23, 2018
53efa39
Specify GADT record syntax
aspiwack Mar 23, 2018
81d6a85
An alternative linear arrow
aspiwack Mar 23, 2018
ed18244
Fix anchor
aspiwack Mar 23, 2018
44105e1
Specifying typechecking of equations
aspiwack Mar 23, 2018
ae45ca7
A note regarding the formalisation of Core
aspiwack Mar 23, 2018
75a5de9
Normalise adornment
aspiwack Mar 23, 2018
9bb678d
Reorder syntax alternative section + add an alternative parsing rule
aspiwack Apr 20, 2018
3e30291
Clarify the alternative notations for arrows
aspiwack Apr 20, 2018
013022a
Improve syntax disclaimer
aspiwack Apr 20, 2018
c2d534b
Relegate η-expansion to an alternative
aspiwack Apr 27, 2018
43ef657
Polymorphisation of constructor in presence of more multiplicities
aspiwack May 4, 2018
9a473d3
Typo
aspiwack May 4, 2018
3bf7953
New rule for constructors
aspiwack May 4, 2018
3d86539
Monomorphisation or multiplicity variables
aspiwack May 4, 2018
d1184a1
Typo
aspiwack May 4, 2018
c0bb7eb
Resolve: typing of pattern matching in Core
aspiwack May 4, 2018
d937a5c
Tweaks to core (in particular mention join points)
aspiwack May 4, 2018
33647fd
Typo
aspiwack May 4, 2018
2a93456
Small fix in view of the new typing rules in Core
aspiwack May 4, 2018
59df6e8
RST fixes
aspiwack May 9, 2018
4678b92
Highlight the main differences between the proposal and the paper
aspiwack May 9, 2018
326844d
Add @mpickering + more detailed implementation plan
aspiwack May 9, 2018
25c9c2e
Add link to Linear Core document
aspiwack May 9, 2018
44b2ca7
Printing strategy and flags
aspiwack Jul 9, 2018
27430dd
Forward ref to Without -XLinearTypes in GADT-syntax specification
aspiwack Jul 9, 2018
350520b
Strict and unpacked fields
aspiwack Jul 9, 2018
03662a3
Reminder that 0≰1
aspiwack Jul 9, 2018
aa732c2
Specification of more pattern forms
aspiwack Jul 9, 2018
11f05cc
Clarify the effects of using linear arrows in APIs
aspiwack Jul 9, 2018
a106fb5
Remove a paragraph from a former version
aspiwack Jul 9, 2018
b027d94
Correct arity for type families (:+) and (:*)
aspiwack Jul 9, 2018
ecf2fb8
Typo
aspiwack Jul 10, 2018
b1016c7
Be more specific about record projections
aspiwack Jul 10, 2018
d3bcafa
Add (|p->) alternative syntax for multiplicity-parametric arrows
aspiwack Jul 10, 2018
61019f8
Fix: section levels
aspiwack Jul 20, 2018
499614a
Clarify wording
aspiwack Jul 20, 2018
82b0e96
Clarify definition of "consume exactly once"
aspiwack Aug 3, 2018
5fa3391
Binders in surface-language let blocks can have varying multiplicity
aspiwack Aug 3, 2018
503fd5e
Specify "consuming" exactly once for unlifted types
aspiwack Aug 3, 2018
2c7dd29
Add @davemenendez syntax proposal
aspiwack Aug 3, 2018
2b85966
Specify pattern-matching of existentially quantified multiplicities
aspiwack Aug 3, 2018
9aa5e43
Some more words on inference
aspiwack Aug 3, 2018
b9e28d9
Typo
aspiwack Aug 6, 2018
9ce6987
typo
adlaika Oct 22, 2018
7c75fd2
Merge pull request #4 from docmoxie/patch-1
mboes Oct 22, 2018
75cc4f2
Move the discussion about exceptions to Effect and interactions
aspiwack Jan 9, 2019
31b930f
Typos and imprecisions
aspiwack Jan 9, 2019
2ce779a
Interactions: no linear arrows in kinds
aspiwack Jan 16, 2019
be9bb31
Add a discussion of a litfIO primitive in RIO
aspiwack Jan 16, 2019
a78ad5a
A number of clarifications on RIO's catch
aspiwack Jan 16, 2019
ca2c75a
Extend the alternatives section
aspiwack Jan 17, 2019
1d4815d
Alternative names for multiplicities
aspiwack Jan 17, 2019
194e840
Finish an unfinished sentence
aspiwack Jan 17, 2019
7e93d29
Syntax: adopt the `a # p -> b` proposal
aspiwack Mar 22, 2019
369248b
Syntax: add BNF modification from the report
aspiwack Apr 5, 2019
5cea37b
Remnant of a grammar proposal past
aspiwack Apr 26, 2019
5eeeed9
Second iteration of the grammar proposal
aspiwack Apr 26, 2019
b875e16
Use the decided-upon syntax
aspiwack Aug 16, 2019
2b29674
Add conditional acceptance to proposal text
goldfirere Apr 3, 2020
f774a19
Formatting
goldfirere Apr 3, 2020
6edfe1b
Update proposals/0000-linear-types.rst
aspiwack Apr 6, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view