0.9

CHANGES:

Version 0.9 (Burghmuirhead) presents multiple major new features, bugfixes, as
well as significant changes and improvements to the Links internals.

Major Changes

Model-View-Update

Links now includes a Model-View-Update library for writing client code, as
pioneered by the Elm programming langauge. More can be found on
the Wiki page.

Relational Lenses: Dynamic Predicates and Typechecking

The implementation of relational lenses has been extended to support dynamic
predicates in select queries. Additionally, much work has been done in order
to allow better typechecking of relational lenses.

Mutual Blocks

Mutually-recursive functions and types should now be enclosed in a mutual
block:

mutual {
  typename Even = [| Z | SuccE:Odd |];
  typename Odd = [| SuccO:Even |];

  sig three : () -> Odd
  fun three() {
    SuccO(SuccE(SuccO(Z)))
  }
}

This leads to significant improvements with the performance of the typechecker
when considering mutually-recursive types, simplifies the code, and solves
multiple bugs.

FreezeML

FreezeML is a new approach to integrating first-class, System F-style
polymorphism with ML-style type inference. The system relies on not guessing
polymorphism, and the ability to "freeze" variables in order to suppress
instantiation. See the TyDe abstract for more details.

Version 0.9 includes an implementation of FreezeML:

• Frozen variables (i.e., variables which are not instantiated) are written
  ~e
• Frozen lets (i.e., function definitions which never generalise their types)
  are written ~fun f(x) { x }
• Explicit function generalisation is written $(fun(x) { x } and produces a
  term of type forall a::Any,b::Row. (a) -b-> a
• Explicit instantiation is written using @

The previous work on "explicit quantification" has been removed.

Effect Sugar

If the effect_sugar flag is set, there are many improvements which decrease
the number of times where explicit effect variables are required.

• Fresh effect variables are no longer generated by the parser
• Higher-order functions share an effect variable with their calling context: for example,
  map : ((a) -e-> b, [a]) -e-> [b] can be written as map : ((a) -> b, [a]) -> [b].
• Type names can now be written with an implicit effect variable, for example
  typename Comp(a) = () ~> a can be written insetad of Comp(a, e::Eff) = () ~e~> a, and forever : Comp(()) ~> ()can be written instead offorever : Comp((), e) e> ()`
• Presence variables can be omitted from effects. As an example, we can
  write

  sig evalState : (s) ->
                (Comp(a, {Get:s,Put:(s) {}-> () |_})) ->
                 Comp(a, {                      |_})
  

  instead of

  sig evalState : (s) ->
                (Comp(a, {Get:s,Put:(s) {}-> () |_})) ->
                 Comp(a, {Get{_},Put{_}         |_})
  

Non-user-visible changes

Much work on 0.9 has concentrated on significant non-user-visible changes. In
particular:

• Desugaring passes which occur after the typechecker are now type-preserving
• Changes to internal representation of types
• Many internal refactorings

Minor Changes

Module system changes

• Modules now work better on the REPL

• import is now used to allow a module to be used in the current file,
  whereas open brings it into the global scope. To get the previous
  behaviour, use open import X for a module X. (breaking change)

• Many behind-the-scenes improvements and bugfixes

Other minor changes

• Compilation on OCaml 4.08 now supported
• select queries now printed when debugging enabled
• Query shredding now supported in SQLite
• The End session type is now linear, and must be eliminated using close.
  This solves a class of memory leaks with session-typed applications.
• Record field punning is now supported. For example, instead of writing
  var hello = "hi"; (hello = hello, world="universe"), it is now possible to
  write var hello = "hi"; (=hello, world="universe").
• lines, unlines, partition, and span added to prelude
• Hyphenated HTML attributes are now allowed
• "Primed" variables such as x' are now allowed
• Initial (hacky) support for null integers in the database. If
  the coerce_null_integers setting is set to true, then null_integer
  (default -1) will be used instead of crashing at runtime.
• Fix draggable list (sessions), draggable cropping frame examples