enso-org/enso
1
1
Fork 0
mirror of https://github.com/enso-org/enso.git synced 2024-09-11 13:15:52 +03:00
Code Issues Projects Releases Wiki Activity

Clarify the syntax for type operators (#811)

Browse Source
This commit is contained in:
Ara Adkins 2020-06-05 13:26:16 +01:00 committed by GitHub
parent c8438fa77b
commit 2e0578d1b3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 212 additions and 47 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
docs/README.md
View File

@ -15,7 +15,7 @@ design, specification, and implementation of the feature to which it pertains.
We provide a number of useful resources for getting a quick understanding of
the Enso project:
- [**The Enso Philosophy:**](./enso-philosophy.md) Information on the design
- [**The Enso Philosophy:**](./enso-philosophy.md) Information on the design
philosophy behind Enso, and why we build things in the way we do.
- [**Contributing Guidelines:**](./CONTRIBUTING.md) Information for people
wanting to contribute to Enso (in many different ways).
@ -41,3 +41,4 @@ It is broken up into categories as follows:
- [**Syntax:**](./syntax) A specification of Enso's syntax.
- [**Types:**](./types) A specification of Enso's type system and type theory.
- [**Debugger:**](./debugger) A specification of Enso's debugger.

148
docs/syntax/types.md
View File

@ -26,6 +26,10 @@ is a useful way of thinking about things when discussing type signatures.
<!-- MarkdownTOC levels="2,3" autolink="true" -->
- [Type Signatures](#type-signatures)
- [Type Operators](#type-operators)
- [Typeset Literals](#typeset-literals)
- [Writing Type Signatures](#writing-type-signatures)
- [Behaviour of Type Signatures](#behaviour-of-type-signatures)
- [Operations on Types](#operations-on-types)
- [Type Definitions](#type-definitions)
- [Visibility and Access Modifiers](#visibility-and-access-modifiers)
@ -59,6 +63,150 @@ Type signatures in Enso have some special syntax:
/ : Number -> Number -> Number ! ArithError
```
### Type Operators
Please note that `:`, `in`, and `!` all behave as _standard operators_ in Enso.
This means that you can section them, which is incredibly useful for programming
with types. In addition, Enso supports a number of additional operators for
working with types. These are listed below.
| Operator | Precedence Relations | Level | Assoc. | Description |
|:--------:|:-----------------------------:|:-----:|:------:|:----------------------------------------------------------------------------|
| `:` | `> =` | 0 | Left | Ascribes the type (the right operand) to the value of the left operand. |
| `in` | `> :`, `> !` | 3 | Left | Ascribes the context (the right operand) to the value of the left operand. |
| `!` | `> :`, `> ->` | 2 | Left | Combines the left operand with the right operand as an error value. |
| `->` | `> :` | 1 | Left | Represents a mapping from the left operand to the right operand (function). |
| `<:` | `> !`, `< |`, `> in` | 4 | Left | Asserts that the left operand is structurally subsumed by the right. |
| `~` | `== <:` | 4 | None | Asserts that the left and right operands are structurally equal. |
| `;` | `< :`, `> =` | -2 | Left | Concatenates the left and right operand typesets to create a new typeset. |
| `|` | `> <:`, `> !`, `> in`, `> :` | 6 | None | Computes the union of the left and right operand typesets. |
| `&` | `= |` | 6 | None | Computes the intersection of the left and right operand typesets. |
| `\` | `< |`, `> <:` | 5 | None | Computes the subtraction of the right typeset from the left typeset. |
| `:=` | `< :`, `> =`, `> ;` | -1 | Left | Creates a typeset member by assigning a value to a label. |
Solving this set of inequalities produces the _relative_ precedence levels for
these operators shown in the table above. In order to check this, you can use
the following formula as an input to an SMTLib compatible solver. For reference,
bind (`=`) has a relative level of -3 in this ordering.
```lisp
(declare-fun ascrip () Int) ; `:`
(declare-fun bind () Int) ; `=`
(declare-fun in () Int) ; `in`
(declare-fun err () Int) ; `!`
(declare-fun fn () Int) ; `->`
(declare-fun sub () Int) ; `<:`
(declare-fun eq () Int) ; `~`
(declare-fun tsConcat () Int) ; `;`
(declare-fun tsUnion () Int) ; `|`
(declare-fun tsInter () Int) ; `&`
(declare-fun minus () Int) ; `\`
(declare-fun tsMember () Int) ; `:=`
(assert (> ascrip bind))
(assert (> in ascrip))
(assert (> in err))
(assert (> err ascrip))
(assert (> err fn))
(assert (> fn ascrip))
(assert (> sub err))
(assert (< sub tsUnion))
(assert (> sub in))
(assert (= eq sub))
(assert (< tsConcat ascrip))
(assert (> tsConcat bind))
(assert (> tsUnion sub))
(assert (> tsUnion err))
(assert (> tsUnion in))
(assert (> tsUnion ascrip))
(assert (= tsInter tsUnion))
(assert (< minus tsUnion))
(assert (> minus sub))
(assert (< tsMember ascrip))
(assert (> tsMember bind))
(assert (> tsMember tsConcat))
(check-sat)
(get-model)
(exit)
```
A permalink to the program using an online Z3 console can be found
[here](https://rise4fun.com/Z3/e99K).
> The actionables for this section are:
>
> - Decide which of these should be exposed in the surface syntax.
### Typeset Literals
Sometimes it is useful or necessary to write a typeset _literal_ in your code.
These work as follows.
- **Typeset Member:** Syntax for typeset members have three components:
+ **Label:** The name of the member. This must always be present.
+ **Type:** The type of the member. This need not be present.
+ **Value:** A value for the member. This need not be present.
This looks like the following:
```ruby
label : Type := value
```
- **Member Concatenation:** Members can be combined into a typeset using the
concatenation operator `;`.
```ruby
x ; y
```
- **Typeset Literals:** A literal can be written using curly braces (`{}`) to
delimit the literal.
```ruby
{ x: T ; y: Q }
```
Typeset literals are considered to be a
[pattern context](./naming.md#pattern-contexts), and hence the standard rules
apply.
### Writing Type Signatures
When ascribing a type to a value, there are two main ways in which it can be
done. Both of these ways are _semantically_ equivalent, and ascribe the type
given by the signature (to the right of the `:`) to the expression to the left
of the `:`.
1. **Inline Ascription:** Using the type ascription operator to associate a
type signature with an arbitrary expression.
```ruby
my_expr : Type
```
2. **Freestanding Ascription:** Using the type ascription operator to
associate a type with a name. The name must be defined on _the line below_
the ascription.
```ruby
a : Type
a = ...
```
3. **Binding Ascription:** Using the type ascription operator to associate a
type with a binding at the binding site.
```ruby
a : Type = ... # this is equivalent to the above example
(a : Type) -> ... # use in a lambda
```
> The actionables for this section are:
>
> - In the future do we want to support freestanding ascription that isn't
> directly adjacent to the ascribed value?
### Behaviour of Type Signatures
In Enso, a type signature operates to constrain the values that a given variable
can hold. Type signatures are _always_ checked, but Enso may maintain more
specific information in the type inference and checking engines about the type

108
docs/types/hierarchy.md
View File

@ -19,6 +19,7 @@ for Enso to _feel_ like a dynamic language while still bringing enhanced safety.
- [Typeset Operators](#typeset-operators)
- [Typeset Subsumption](#typeset-subsumption)
- [Unsafe Typeset Field Mutation](#unsafe-typeset-field-mutation)
- [Dependent Lists](#dependent-lists)
- [Interfaces](#interfaces)
- [Special Interfaces](#special-interfaces)
- [Type Ascription](#type-ascription)
@ -48,8 +49,8 @@ specificity.
7 : 7 : Natural : Integer : Number : Any : Any : ...
```
A brief note on naming (for more, please see the
[naming syntax](../syntax/naming.md):
A brief note on naming (for more, please see the
[naming syntax](../syntax/naming.md)):
- Naming in Enso is case-insensitive.
- In contexts where it is ambiguous as to whether the user would be referring to
@ -90,34 +91,27 @@ share some similarities with records they are a far more general notion.
- A typeset is an entity that contains one or more labels.
- Each label has a type, which _may_ be explicitly ascribed to it.
- Each label may have a default value provided for it.
- A label may be _duplicated_, as long as the types of the duplicate labels are
different.
- Each label may have a value provided for it.
The other key notion of typesets is that typesets are matched _structurally_,
subject to the rules for nominal typing of atoms discussed above.
The definition for a typeset member uses the syntax `label : type = val`, where
the following rules apply:
- If a default is explicitly requested it becomes part of the subsumption
judgement (see [below](#typeset-subsumption)).
- If the type of a label is omitted it is inferred from a default if present,
and is otherwise inferred to be `Any`.
- If only the type is present, auto-generated labels are provided using the
index of the member in the typeset (e.g `{ Int, String }.1` has type `Int`).
These labels act specially for unification.
- Labels are syntactically _names_, but internally may be other entities (e.g.
types).
- A typeset member is itself a typeset.
- Typeset members are themselves typesets.
- A typeset member _must_ have a label, but may also have a type and a value
(`label : Type := value`)
- An unspecified type is considered to be a free type variable.
- The label and the type become part of the typing judgement where present, and
will be used for unification and subsumption.
Typesets themselves can be declared in two ways:
1. **Anonymous:** An anonymous typeset can be declared using the curly-braces
syntax `{}`. Such a definition must contain zero or more typeset fields (see
above).
2. **Atoms:** An atom definition declares a typeset with a discrete identity,
using atom definition syntax. Atom fields must only be names.
1. **Anonymous:** An anonymous typeset can be declared using the curly-braces
syntax `{}`. Such a definition must contain zero or more typeset fields (see
above). Please note that `{}` is necessary as it needs to delimit a pattern
context.
2. **Atoms:** An atom definition declares a typeset with a discrete identity,
using atom definition syntax. Atom fields must only be names.
3. **Concatenation:** Combining two typeset values using `;`.
Typesets can be combined using the [typeset operators](#typeset-operators)
defined below.
@ -126,10 +120,6 @@ In addition, we provide syntactic sugar for defining typesets as described in
the syntax document. This syntax has a special desugaring that obeys the
following rules:
> Actually fill in these rules.
> Note that because things desugar to functions we can place arbitrary
constraints on initialisation (partial type constructors style).
```ruby
type Maybe a
Nothing
@ -169,30 +159,44 @@ Just.nothing = not isJust
> The actionables for this section are as follows:
>
> - Simplify this definition if we decide _not_ to support multiple dispatch.
> - Determine how duplicate labels should work, and if it should work.
> - Note that because things desugar to functions we can place arbitrary
> constraints on initialisation (partial type constructors style).
### Typeset Operators
Enso defines a set of operations on typesets that can be used to combine and
manipulate them:
manipulate them. Any use of these operators introduces typing evidence which
may later be discharged through pattern matching.
- **Subsumption - `<:`:** This operator expresses the relation between typesets
defined below in the section on [typeset subsumption](#typeset-subsumption).
- **Equality - `~`:** This operator expresses the relation that two typesets `a`
and `b` are equal (such that `a <: b && b <: a`).
- **Concatenation - `,`:** This operator combines multiple typesets, and is most
often used to combine typeset fields. It expresses product types.
- **Union - `|`:** This operator creates a typeset that contains all the types
in the union of its operand typesets.
- **Intersection - `&`:** This operator creates a typeset that contains all the
types in the intersection of its operand typesets.
- **Subtraction - `\`:** This operator creates a typeset that contains all the
types in its first operand that are _not_ also contained in its second
operand.
- **Function - `->`:** This operator creates a mapping from one typeset to
another, and its result is a typeset containing all the possible types of that
mapping.
They are as follows:
Any use of these operators introduces typing evidence which may later be
discharged through pattern matching.
- **Type Ascription - `:`:** This operator ascribes the type given by its right
operand to the expression of its left operand.
- **Context Ascription - `in`:** This operator ascribes the monadic context
given by its right operand to the expression of its left operand.
- **Error Ascription - `!`:** This operator combines the type of its left
operand with the error type of its right. This is _effectively_ an `Either`,
but with `Left` and `Right` reversed, and integrates with the inbuilt
mechanism for [broken values](../semantics/errors.md#broken-values).
- **Function - `->`:** This operator defines a mapping from one expression to
another.
- **Subsumption - `<:`:** This operator asserts that the left hand operand is
_structurally subsumed_ by the right-hand operand. For more details on this
relationship, see [typeset subsumption](#typeset-subsumption) below.
- **Equality - `~`:** This operator asserts that the left and right operands are
structurally equal.
- **Concatenation - `;`:** This operator combines multiple typesets, expressing
product types.
- **Union - `|`:** This operator creates a typeset that contains the members in
the union of its operands.
- **Intersection - `|`:** This operator creates a typeset that contains the
members in the intersection of its operands.
- **Subtraction - `\`:** This operator creates a typeset that contains all of
the members in the left operand that do not occur in the right operand.
For information on the syntactic usage of these operators, please see the
section on [type operators](#../syntax/types.md#type-operators) in the syntax
design documentation.
> The actionables for this section are:
>
@ -200,6 +204,7 @@ discharged through pattern matching.
> these operators.
> - When do applications of these constructors create matchable (injective and
> generative) types?
> - Are `<:` and `:` equivalent in the surface syntax?
### Typeset Subsumption
For two typesets `a` and `b`, `a` is said to be subsumed by `b` (written using
@ -272,6 +277,17 @@ themselves, but as atoms are typesets this also applies.
- In order to prevent this from being used flippantly, this functionality is
marked `unsafe` (see [access modifiers](./access-modifiers.md) for more).
## Dependent Lists
The most-specific type of an Enso list is the list of the types of the list's
elements. By way of example, the following are true:
```ruby
[1, 1.2, "String"] : List [Integer, Number, String] : List [Number, Number, String] : ...
[1, 1.2, 3.0f] : List [Integer, Number, Double] : List [Number, Real, Real] : List Number : ...
```
This means that Enso's lists _fully subsume_ the use cases for standard tuples.
## Interfaces
Because typesets can be matched _structurally_, all typesets implicitly define
interfaces. A type `t` conforming to an interface `i` in Enso is as simple as