-
Notifications
You must be signed in to change notification settings - Fork 35
/
changelog
161 lines (130 loc) · 6.57 KB
/
changelog
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
# 0.9.5.0
- Rank N typing (see https://github.com/granule-project/granule/blob/dev-minor/examples/rankN.gr)
- Algebraic effects and handlers. See e.g.,
* https://github.com/granule-project/granule/blob/dev-minor/examples/effects_nondet.gr
* https://github.com/granule-project/granule/blob/dev-minor/examples/effects_state.gr
- Updated standard docs
- Fixes to deriving copyShape and drop combinators
- push deriving combinators now have Pushable constraint, e.g.
pushList : forall {s : Semiring, r : s, a : Type}
. {(1 : s) <= r, Pushable r} => (List a) [r] -> List (a [r])
pushList = push @List
- Minor tweaks to the Granule Language Server to improve vscode interaction (no longer complains on the entire file about 'Premature end of file' whilst typing).
# 0.9.4.0
- Advanced synthesis algorithm for `language GradeBase` mode.
- Better standard library documentation
- Ability to expose the 'hsup' constraint (see `push`)
- Some bug fixes (see https://github.com/granule-project/granule/milestone/2?closed=1)
# 0.9.3.0
- Existential types, e.g.,`exists {x : Type} . t`, see `examples/existential.gr` and `examples/listToVec.gr`
- `language GradedBase` extension, see `examples/graded-base.gr`
- Various internal refactorings
- Bug fixes related to indexed types
- Uniqueness features renamed (see `examples/uniqueness.gr`)
- Granule docs's feature `gr --grdoc file.gr` will generate documentation in `docs/index.html`
# 0.9.2.0
- New `Cartesian` semiring, with just one element `Any : Cartesian` for completely erasing grading (trivial solving)
- (Internal)
- Restructuring to tests
# 0.9.1.0
- Public and Private are now usable as synonyms for Lo and Hi unless the SecurityLevels extension is turned on.
- 'Level' semiring only in scope when SecurityLevels extension is on.
- Builds on ghc 9.2 now
# 0.9.0.1
- Bug fixes to pretty printer
- forkNonLinear can only work over semirings with exact equality for soundess
- Tweaks to the way type-level float equality works
# 0.9.0.0
- Major features:
- Uniqueness modality and mutable arrays
- https://granule-project.github.io/papers/esop22-paper.pdf
- Session types with non-linear behaviours
- https://arxiv.org/abs/2203.12875
- Granule -> Haskell compiler (grc)
- language-server protocol
- New graded modalities / improvements
- LNL semiring (Zero, One, Many) recovers linear logic via new `hsup` operation
to control 'push' behaviour on tensors. See: https://granule-project.github.io/papers/tlla_2021_paper11.pdf
- Any semiring can now be lifted to a top-completed semiring with Ext (previously only allowed for Nat)
- Language extensions and pragmas: See: https://github.com/granule-project/granule/wiki/Language-Extensions
- Includes CBN interpreter as an option
- Bug fixes:
- Bug fixes related to sensitivity analysis
- Bug fixes relating to derived operation copyShape
- Improved interpreter
- Tons of minor improvements
- Error messages are sometimes more intuitive
- Various additional primitives
# 0.8.1.0
- New semirings: `Sec` and `Set t` for some type `t` (and `SetOp t`)
- Bug fixes related to session types
- Some more type aliases added
- Generic deriving coverage improved (especially with `drop`)
# 0.8.0.0
- --synthesise mode
- Support for deriving simple distributive laws
- Improved error messages
- Improved dependent kinds support
- Automatic case splitting and code rewriting features
- `case` in types
- New OOZ (One or Zero) semiring
# 0.7.7.2
- LLVM compiler separated into its own project to make building easier at the moment (see https://github.com/granule-project/granule-compiler-llvm).
- Built-ins now get internally kind checked earlier, reducing the chance of us making malformed built-ins.
- A couple of missing examples and tests added.
- `case` expressions are now restricted to matching on non-indexed data types, with a helpful messages (this avoids pitfalls with dependent case)
- Various small bug fixes.
# 0.7.7.1
- Some small fixes
- Tweaks to improve error messages
# 0.7.7.0
- Standard library changes
- `Cake`: back in to StdLib
- `Choice`: new library (provides linear tensor)
- `Prelude` change: generalised `pull`, `comp`, `unbox`
- `Vec` addition: `pushVec`
- `Graph` bug fixes: `size` and `vertexcount` changed due to a bug fix in Granule;
- Modules can now have headers where data constructors can be hidden on export,
e.g. module Cake hiding (Cake, Happy) where...
- Fixed some bugs in `grepl` (now reads the .granule config file instead of its own)
- `grepl` can now give the type of general expressions (if the checker can infer it)
- Various refactorings in the compilation of constraints to SMT; fixes a bug with `Graph` lib
# 0.7.6.0
- LLVM compiler for a simple subset now included.
- Various internal changes which allow effect modalities (graded possibility) to be richer.
- Type-level sets support improved with some syntax changes, e.g., <{Read, Write}>.
- Nat-graded monads now provided.
- Some renaming, R and W replaced with Stdin and Stdio so as to avoid conflicts with HandleType.
- More flexibility when combining different grading types.
- Type holes.
- `grin` renamed to `grepl`.
- Various tweaks to the standard library and various bug fixes.
# 0.7.2.0
- Ability to include additional predicates in type signatures
- More pervasive unicode support
- Support fewer type annotations
- Literate mode for LaTeX/Granule files
- Integers can be linearly consumed in patterns
- Some bug fixes
# 0.7.1.0
- Various improvements to error reporting
- New features for allowing interacting between coeffects due to nested unboxing
- Bug fixes on linearity in nested cases expressions
- FileIO modality renamed to IO
- Some internal reworking of security levels to match the theory
# 0.7.0.0
- Functions can now be written as a set of equations, and this is the best way to get dependent pattern matching
- Various key bug fixes
- Existentials
# 0.6.0.5
- IOMode is now a primitive type rather than being used primitively but being defined in a library
# 0.6.0.4
- Improved type support in `grin`
- Refactoring to how ASTs are internally represented
- Some fixes regarding consumption effects in pattern matches.
# 0.6.0.1
Simplified internals of kinds and coeffect types
# 0.6.0.0
Granule REPL added, called 'grin'
# 0.5.5.7
Session type duality and fork, forkRep, send, recv, close primitives.