mirror of https://github.com/enso-org/enso.git synced 2024-12-24 08:42:05 +03:00

History

Jaroslav Tulach 7998ed5218 case of and intersection types (#11850 ) Also: Prefer `getURI` path when gathering location of a source		2024-12-13 16:02:51 +01:00
..
access-modifiers.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
contexts.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
dynamic-dispatch.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
errors.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
evaluation.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
function-types.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
goals.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
hierarchy.md	Intersection types & type checks (#11600 )	2024-12-12 07:29:00 +00:00
inference-and-checking.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
intersection-types.md	case of and intersection types (#11850 )	2024-12-13 16:02:51 +01:00
modules.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
parallelism.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
pattern-matching.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
README.md	Intersection types & type checks (#11600 )	2024-12-12 07:29:00 +00:00
references.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
type-directed-programming.md	Adding "Warnings note" to suspicious sections in types documentation. (#11775 )	2024-12-07 07:50:00 +01:00
types.md	Add type system documentation (#3376 )	2022-08-15 18:36:03 +03:00

README.md

layout

title

Enso's Type System

On the spectrum of programming type systems ranging from dynamically typed to statically typed, one likes to think that there is a happy medium between the two. A language that feels dynamic, with high levels of type inference, but lets the users add more type information as they want more safety and compile-time checking.

Enso aims to be that language, providing a statically-typed language with a type system that makes it feel dynamic. It will infer sensible types in many cases, but as users move from exploratory pipelines to production systems, they are able to add more and more type information to their programs, proving more and more properties using the type system. This is based on a novel type-inference engine, and a fusion of nominal and structural typing.

All in all, the type system should stay out of the users' ways unless they make a mistake, but give more experienced users the tools to build the programs that they require.

This document contains discussion and designs for the type-system's behaviour, as well as formal specifications where necessary. It discusses the impact of many syntactic language features upon inference and type checking, and is instrumental for ensuring that we build the right language.

Note

A Note on Syntax

In the aid of precision, this document will use syntax that may not be exposed to users. The appearance of a piece of syntax here that is not described in the syntax document makes no promises as to whether said syntax will be exposed in the surface language.

Warning

The specification in this section is very outdated and far from reality. Sections that are known to be "off" are marked as warning.

Information on the type system is broken up into the following sections:

Goals for the Type System: The goals for the Enso type system, particularly around usability and user experience.
The Type Hierarchy: The type hierarchy in Enso.
Intersection Types: intersection types in Enso.
Function Types: Function types in Enso.
Access Modification: Access modifiers in Enso (e.g. private and unsafe),
Pattern Matching: The typing of pattern match expressions in Enso.
Dynamic Dispatch: How dynamic dispatch interacts with the type system in Enso.
Modules: A description of the Enso module system.
Monadic Contexts: A description of the typing and functionality of Enso's monadic contexts.
Strictness and Suspension: A description of how the type system interacts with Enso's evaluation semantics.
Analysing Parallelism: A description of how the type system interacts with the planned automated parallelism analysis.
Type-Directed Programming: A description of how the type system aids type-directed programming, and the features it has to support this approach.
Errors: The interaction between Enso's errors and the type system.
Type Inference and Checking: A description of Enso's type inference and checking system.
References: Useful references for working on the type system and its theory.