\forall or constraints). Custom labels that are
disjoint from all others can be created via newtype.self. Their technique
allows later adding extra fields and methods to the object, and
re-sealing it so that new methods have access to the new
fields. They also provide a complete type inference algorithm (there
are no type annotations in the language).principal typings with rank-2 intersection types
non-exhaustive list of value-level features
'a . bottom ->
'a)if.l), update (with existing_l = v), addition (with
new_l = v), deletion (without l)f -> g | h -> i, and a record with labels {f,h},
uniformly mapping the function on the record gives a new record
{g,i}λ r l -> r.l takes a record and a label, and
accesses the given label in the recordcontains constraint or type with some fixed labels and a row for
the restlacks constraint (ensure that some labels are absent from the
row)disjoint constraint (to ensure that concatenation does not cause
duplicate labels)included-in constraintWhen the language has an effects system or linear type system, it is
necessary to ensure that row operations are safe. For example, if the
fields in the row are duplicated via let x = {z with f = 1} and y =
{z with f = 2} in …, it is necessary to ensure that none of these
fields were constrained by the linear type system.
I think it would be best to implement the type system of ROSE, and try to add row maps ("transformation" above) and first-class labels.
The environment is:
* a stack of lexical scopes with local variables (let or function arguments).
* lexical scopes and references introduced by hygienic macros, which
exist on a sort of parallel stack for each macro
invocation. Macro-defining macros are more complex to understand
(see http://www.cs.utah.edu/plt/scope-sets/ for more)
* identifiers introduced by opening modules (globally via open X,
locally via let open X in expr, or X.expr)
Non-macro lexical scopes and module interfaces can be thought of as row operations (usually in a model where shadowing is allowed).
Uses of macros: * Inlining. This is better done by an "inline" directive. * Abstraction of repetitive boilerplate that cannot be expressed using function or other basic language abstractions. Better solution would be to not have second-class language constructs that cannot be abstracted over. * Optimizations on the generated code. * Changing the order of evaluation (lazy vs. eager) * The creation of new binding forms
macro expansion = one level of partial expansion
Metaprogramming facilities (macros or environment-manipulating functions) may need to introduce fresh identifiers for temporary variables or for behind-the-scenes communication between two uses of a macro to track information across these invocations.
Traditionally, LISP programs use gensym to create a fresh
(preferably uninterned) symbol. We need a way to give a type to a
gensym-like function.
Nominal typing provides a way to create a unique identifier that can be used for that purpose. However, for macros that produce macros, one needs a way to generate fresh identifiers on the fly, instead of having a fixed set of pre-declared unique identifiers.
It is therefore desirable to be able to express in row constraints the fact that a certain label will e.g. be absent from arguments and present in a returned row, indicating that this label is fresh (and therefore that it is trivially absent from arguments). This is very similar to how existential types allow hiding information to unprivileged parts of the code.
Detecting uninhabited types can be difficult depending on the type system.
Uninhabited types can cause spurious "pattern-matching does not cover all cases" errors (since some cases may be impossible but not detected as such)
Ex Falso Quodlibet might be a problem in some type systems. If the type system assumes that types are always inhabited, but is unable to always detect uninhabited types, then there is a problem.
self argument to
methods). These aspects should be orthogonal.message-passing: when calling the method on the receiver, the receiver itself should be passed, usually as the first argument.
static dispatch decides which case of an overloaded function is called at compile-time, based on the static type information available.
dynamic dispatch decides which implementation of a method is called at run-time, based on the dynamic type of the object.
Single dispatch: at run-time, the instance of the receiver is used
to determine the implementation of the method. E.g. in x.m, if x
has dynamic type Foo then the implementation of m in Foo is
used, even if the static type of x is a supertype of Foo
(e.g. via a type annotation)
m to
be determined by the dynamic type of the receiver and one or more
arguments, e.g. 1.add(2.0) will select the implementation
add(self: Int, x: Float), but 1.add(2) would select add(self:
Int, x: Int).x.f(y …). Without the import, this call can be handled
by a general case, and the import can make a more specific case
available. This can be solved by enforcing that new cases are
declared in the same module as one of the types involved in their
signature (or in the same module that declares the multimethod
itself, for nominal declarations).
See explanation in the context of Racket's multimethods.Modules: allow ensuring that a specific implementation is used for an operation (e.g. the comparison function for comparable pairs of integers, for which there are several implementations). On the other hand, with typeclasses, one cannot easily mix pairs of integers sorted with different sorting functions within the same program.
Typeclasses: more natural way to describe overloading than using functors.
'a t contains in its definition
'b t, where 'b depends on 'a but is not 'a, e.g. type 'a t
= Tree of 'a | Depth of ('a * 'a) tlet rec or something similar to the y combinator,
causes the unification of a type variable corresponding to the
parameter of the function, and the type of an expression in the body
(the argument passed to the recursive call). The type of this
expression will likely depend on the parameter.
μ
type combinator.a refer to the same field declaration. The IDE
can automate the declaration of these fields.f and apply it to a variety of values.mk f g h = { f = f; g = g; h = h } returns a struct,
if only rank-1 polymorphism is allowed then the types of f, g and h
become weakly polymorphic).A workaround which supports some use cases of rank-N polymorphism
consists in moving all forall type variables to the beginning of the
type (prenex form), and specify via type constraints what concrete
types must be unifiable with these. For example, f g = (g 1) + (g
"hi") can be assigned the type (forall a . a → int) → int. A
constrained prenex form with subtyping would be forall t . (t ≤ int →
int, t ≤ string → int) ⇒ t → int. Other constraints than ≤ can be
used to allow only a limited form of subtyping that compares e.g. if a
function type can be unified with another (a simple check that does
not unify type variables within both sides).
Another workaround that supports some uses cases of rank-N polymorphism is the use of intersection types.
In some cases (probably low-rank polymorphism and / or value
restriction) an expression is assigned a type which is a unification
variable (e.g. empty_list : 'a list as opposed to empty_list :
forall 'a . 'a list). This means that all occurrences of that
variable must unify with the same type.
There is a problem when the expression is used in contexts where it
must unify with distinct types, e.g. let x = empty_list in ((1 :: x),
("hi" :: x)). Either the overall expression will not typecheck, or it
may cause spurious equality constraints to appear.
In that case, a (common?) workaround is to duplicate (immutable) identifiers, so that each use is typechecked as if it came from an independent declaration. This means that occurrences are not forced to have the same type. This strategy can cause a blow-up in the size of the program to effectively typecheck, but there are mitigations for that.
TODO: write about modules
τ ≤ π implies τ' ≤ π', where τ' is determined by
τ in some way (and π' is determined by π). Example: α → β ≤ δ
→ γ implies β ≤ γ (function types are covariant in their return
type).τ ≤ π implies τ' ≥ π', e.g. α → β ≤ δ → γ
implies α ≥ δ (function types are contravariant in their argument
type).Invariant: τ ≤ π implies τ' = π'.
Often occurs because a type variable occurs both in a covariant and a contravariant position.
Richer constraint, polymorphism and subtyping systems are able to avoid placing an equality constraint in some of these cases.
(Γ |- e : τ) ⇒ (Γ |- eval₁(e) : τ)(Γ |- e : τ) ⇒ (Γ |- eval(e) : τ)Γ and e, there is a type scheme
τ such that Γ |- e : τ and any other possible type τ' (such
that Γ |- e : τ') can be obtained by instantiating the type
scheme, i.e. τ' = σ(τ), for some reasonable definition of what σ
can be.e
alone is used to infer both Γ and τ. Allows for bottom-up
inference