(as of v0.8.2.0) Granule has various language extensions which you can turn on with language keyword at the top of a module.
NoTopLevelApprox
Approximation of grades is possible via type signatures that exploit the pre-ordering of grades. For example:
copy : forall {a : Type} . a [0..3] -> (a, a)
copy [x] = (x, x)
With the NoTopLevelApprox extension this is not allowed anymore, which means that type signatures have to be 'tight'. This now fails to type check:
-- Ill-typed
language NoTopLevelApprox
copy : forall {a : Type} . a [0..3] -> (a, a)
copy [x] = (x, x)
But this is fine:
language NoTopLevelApprox
copy : forall {a : Type} . a [2..2] -> (a, a)
copy [x] = (x, x)
This is useful for exploring how approximation is being applied by the type-checker as sometimes approximate grades can be confusing for the programmer in more complex situations (a grading that might be unintended may type-check due to approximation).
CBN (Call-By-Name)
By default, Granule has a call-by-value semantics implemented in the interpreter. However, you can switch it to a call-by-name semantics
with the CBN extension. The difference can only be observed when using linear channels which create implicit side effects.
language CBN
SecurityLevels
This provides access to the Level semiring which interacts differently with pattern matching.