diff --git a/docs/semantics/errors.md b/docs/semantics/errors.md index d66c97d1dfff..42ca7918cef5 100644 --- a/docs/semantics/errors.md +++ b/docs/semantics/errors.md @@ -20,12 +20,31 @@ users to deal with errors at runtime in the language. ## Asynchronous Exceptions +> [!WARNING] > The actionables for this section are: > +> - Why do we call it asynchronous, when they are synchronous!? > - Specify the semantics of Enso's async exceptions. ## Broken Values +There is a special [dynamic dispatch](../types/dynamic-dispatch.md) for `Error` +values. A dataflow error dispatch first checks if it may call a method on +`Error` type. + +> [!WARNING] > The actionables for this section are: > > - Specify the semantics of Enso's broken values. + +## Warnings + +> [!WARNING] +> TODO +> +> - Values in Enso may have warnings attached + +There is a special [dynamic dispatch](../types/dynamic-dispatch.md) for _values +with warnings_. Before we pass the dispatch to the underlying value, +we check if warning has a method 'overridden' - this is used for `remove_warnings`, +etc. diff --git a/docs/types/README.md b/docs/types/README.md index 08505b4e6c52..3cd0c41313f4 100644 --- a/docs/types/README.md +++ b/docs/types/README.md @@ -30,6 +30,8 @@ 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 @@ -37,8 +39,9 @@ instrumental for ensuring that we build the right language. > described in the [syntax](../syntax/README.md) document makes no promises as > to whether said syntax will be exposed in the surface language. -> **Please Note:** The designs in this section are currently very exploratory as -> the type system is not slated from implementation until after 2.0. +> [!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: diff --git a/docs/types/access-modifiers.md b/docs/types/access-modifiers.md index fc0eb8a97fde..9102146c0ff7 100644 --- a/docs/types/access-modifiers.md +++ b/docs/types/access-modifiers.md @@ -8,83 +8,54 @@ order: 4 # Access Modifiers -While we don't usually like making things private in a programming language, it -sometimes the case that it is necessary to indicate that certain fields should -not be touched (as this might break invariants and such like). To this end, Enso -provides an explicit mechanism for access modification. +> [!WARNING] +> Everybody who ever maintained a large system knows [encapsulation is essential](../semantics/encapsulation.md). +> +> While we don't usually like making things private in a programming language, it +> sometimes the case that it is necessary to indicate that certain fields should +> not be touched (as this might break invariants and such like). To this end, Enso +> provides an explicit mechanism for access modification. + +Enso targets large user base of _non-programmers_. They are mostly focused on +getting their job done and [encapsulation](../semantics/encapsulation.md) of their own code is the last thing +that comes to their mind. + +On the other hand, Enso supports and encourages creation of *sharable libraries*. +Maintainers of such libraries are likely to treat API design and its +backward compatibility seriously. As such they need a way to [encapsulate](../semantics/encapsulation.md) +internals of their libraries and clearly *differentiate public API* and +implementations details. - [Access Modification](#access-modification) - [Private](#private) -- [Unsafe](#unsafe) ## Access Modification -Access modifiers in Enso work as follows: - -- We have a set of access modifiers, namely `private` and `unsafe`. -- We can place these modifiers before a top-level definition. - - ```ruby - type MyAtomType - type MyAtom a - - is_foo : Boolean - is_foo = ... - - private private_method a b = ... - - unsafe unsafe_method a b = ... - ``` - -- By default, accessing any member under an access modifier is an error when - performed from another module. -- To use members protected by an access modifier, you must _import_ that access - modifier from the file in which you want to access those elements. +*By default* Enso elements (functions, types, methods) are *public*. +One has to use an access modifier to hide and [encapsulate](../semantics/encapsulation.md) them. The +reasoning is: those who don't care can access everything they create without +any restriction. Those who care can make things `private` with an additional +effort. - ```ruby - import private Base.Data.Vector - import unsafe Base.Data.Atom - ``` -- These modified imports are available in _all_ scopes, so it is possible to - limit the scope in which you have access to the modified definitions. +Accessing any member under an access modifier is an error when performed from another project. +Such a check is enforced during runtime. - ```ruby - function_using_modifiers v x = - import private Base.Data.Vector - import unsafe Base.Data.Atom - - v.mutate_at_index 0 (_ -> x) - x = MyAtom.mutate_field name="sum" (with = x -> x + 20) - x + 20 - ``` - -> The actionables for this section are: -> -> - How do we type this? +There is a command line switch to _disable access modifier check_. +It maybe be useful for experimentation. However the general suggestion is: +Avoid using it in production. ## Private -The `private` modifier acts to hide implementation details from clients of the -API. It is: - -- Available by default in the `Base` library. -- Able to be avoided using the above-described mechanism. +Encapsulation is an effective _communication mechanism_ among _distributed +groups_ of developers. The `private` modifier hides implementation details from clients of the API. +The primary groups in the Enso case are those who *publish a library* +and those who *consume such a library*. -## Unsafe - -While `private` works as you might expect, coming from other languages, the -`unsafe` annotation has additional restrictions: - -- It must be explicitly imported from `Base.Unsafe`. -- When you use `unsafe`, you must write a documentation comment on its usage - that contains a section `Safety` that describes why this usage of unsafe is - valid. - -> The actionables for this section are: -> -> - Specify `unsafe` properly. +As such Enso supports _library private_ encapsulation. +To hide any element (module, type, constructor, function) away +from *library consumers* prefix such an element with `private` keyword. diff --git a/docs/types/contexts.md b/docs/types/contexts.md index 58984b0bdc0a..bccd3eeac918 100644 --- a/docs/types/contexts.md +++ b/docs/types/contexts.md @@ -8,13 +8,17 @@ order: 8 # Monadic Contexts -Coming from a Haskell background, we have found that Monads provide a great -abstraction with which to reason about program behaviour, but they have some -severe usability issues. The main one of these is the lack of automatic lifting, -requiring users to explicitly lift computations through their monad transformer -stack. - -For a language as focused on usability as Enso is this really isn't feasible. To +> [!WARNING] +> Reword for people without Haskell background who don't know what _lifting_ is. +> +> Coming from a Haskell background, we have found that Monads provide a great +> abstraction with which to reason about program behaviour, but they have some +> severe usability issues. The main one of these is the lack of automatic lifting, +> requiring users to explicitly lift computations through their monad transformer +> stack. + +For a language as focused on usability as Enso is importing all the _complexity +of Haskell monads_ really isn't feasible. To that end, we have created the notion of a 'Monadic Context', which is a monad transformer based on Supermonads (see [references](./references.md#monadic-contexts)). These have special support in @@ -33,8 +37,6 @@ the compiler, and hence can be automatically lifted to aid usability. - [Context Syntax](#context-syntax) - [Monadic Bind](#monadic-bind) -- [Context Definitions](#context-definitions) -- [Context Lifting](#context-lifting) - [Inbuilt Contexts](#inbuilt-contexts) - [IO](#io) - [State](#state) @@ -43,59 +45,70 @@ the compiler, and hence can be automatically lifted to aid usability. ## Context Syntax -There are three main notes about the syntax of contexts: - -1. Monadic contexts are defined using the `in` keyword (e.g. `Int in IO`). -2. We have a symbol `!`, which is short-hand for putting something into the - `Exception` monadic context. This is related to broken values. -3. Contexts can be combined by using the standard typeset operators, or nested - through repeated uses of `in`. +> [!WARNING] +> There used to be three main notes about the syntax of contexts: +> +> 1. Monadic contexts are defined using the `in` keyword (e.g. `Int in IO`). +> 2. We have a symbol `!`, which is short-hand for putting something into the +> `Exception` monadic context. This is related to broken values. +> 3. Contexts can be combined by using the standard typeset operators, or nested +> through repeated uses of `in`. + +There is no special syntax for contexts anymore. +Since [#3828](https://github.com/enso-org/enso/pull/3828) +Enso is no longer relaying on a haskelly solution. +Rather than that _contexts_ are being manupulated by +_standard library_ functions grouped around +`Standard.Base.Runtime.Context` & co. +```ruby +Runtime.Context.Output.with_enabled <| + File.new "c:\trash.txt" . delete +``` + +There is still the `!` symbol signaling [presence of errors](./errors.md) +- e.g. _broken values_. However the runtime can handle _broken values_ +even without presence of these _exception type signatures_. Thus the +compiler only verifies the referenced types are valid. ## Monadic Bind -It is also important to note that Enso has no equivalent to `<-` in Haskell. -Instead, pure computations are implicitly placed in the `Pure` monadic context, -and `=` acts to 'peel off' the outermost layer of contexts. As such, this means -that `=` _always_ acts as `bind`, greatly simplifying how the type-checker has -to work. - -## Context Definitions - -Contexts can be defined by users. - -> The actionables for this section are: -> -> - How, what, when and why? - -## Context Lifting - -> The actionables for this section are: -> -> - Specify and explain how automated lifting of monadic contexts works. -> - It depends on the order of `runCtx` +> [!WARNING] +> Who knows what `<-` means in Haskell? +> +> It is also important to note that Enso has no equivalent to `<-` in Haskell. +> Instead, pure computations are implicitly placed in the `Pure` monadic context, +> and `=` acts to 'peel off' the outermost layer of contexts. As such, this means +> that `=` _always_ acts as `bind`, greatly simplifying how the type-checker has +> to work. ## Inbuilt Contexts -Enso includes a set of commonly-used monadic contexts as part of `Base`, its -standard library. These are listed below. +Enso standard library defines `Input`, `Output` and `Dataflow_Stack_Trace` +contects as of Enso 2024.5.1 version. Users cannot define their own. -> The actionables for this section are: -> -> - Determine the full set of contexts that Enso should provide by default. +### State -### IO +The _state_ concept is implement by standard libraries with _no support in the type system_. -> The actionables for this section are: -> -> - Determine the granularity of IO (it's not one context, but a lot). -> - Explain how there is no `runIO`, and IO is just run at the program boundary, -> as well as the impacts of this. +State acts as a [thread local](https://en.wikipedia.org/wiki/Thread-local_storage) variable +of operating system: + +- an _initializing code_ can set `State` up +- execute some code +- a code somewhere deep the stack (while _initializing code_ is still on the stack) +- may pick the state up +- once the _initializing code_ finishes execution +- the state is gone -### State +It is an example of _tunnelling a value_ from one side (e.g. code) of the "tunnel" to another, +without the "tunnel" (e.g. thee code in between) knowing about it. -> The actionables for this section are: + + +See `Standard.Base.Runtime.State` for more details. diff --git a/docs/types/dynamic-dispatch.md b/docs/types/dynamic-dispatch.md index 013ddfc42fa8..c334b832b25f 100644 --- a/docs/types/dynamic-dispatch.md +++ b/docs/types/dynamic-dispatch.md @@ -13,14 +13,9 @@ for usability, as users can write very flexible code that still plays nicely with the GUI. The current implementation of Enso supports single dispatch (dispatch purely on -the type of `this`), but there are broader visions afoot for the final -implementation of dynamic dispatch in Enso. - -> The actionables for this section include: -> -> - Determining whether we want to support proper multiple dispatch in the -> future. This is important to know as it has implications for the type -> system, and the design of the dispatch algorithm. +the type of `self`) when calling function. When calling (binary) operators Enso +may perform more complicated dispatch when searching for the right operator +implementation to invoke. @@ -36,69 +31,79 @@ one to select, the compiler needs to have a notion of _specificity_, which is effectively an algorithm for determining which candidate is more specific than another. -- Always prefer a member function for both `x.f y` and `f y x` notations. -- Only member functions, current module's functions, and imported functions are - considered to be in scope. Local variable `f` could not be used in the `x.f y` - syntax. -- Selecting the matching function: - 1. Look up the member function. If it exists, select it. - 2. If not, find all functions with the matching name in the current module and - all directly imported modules. These functions are the _candidates_. - 3. Eliminate any candidate `X` for which there is another candidate `Y` whose - `this` argument type is strictly more specific. That is, `Y` this type is a - substitution of `X` this type but not vice versa. - 4. If not all of the remaining candidates have the same this type, the search - fails. - 5. Eliminate any candidate `X` for which there is another candidate `Y` which - type signature is strictly more specific. That is, `Y` type signature is a - substitution of `X` type signature. - 6. If exactly one candidate remains, select it. Otherwise, the search fails. - -> The actionables for this section are as follows: +> [!WARNING] +> Static compiler selects nothing. The right method to invoke is _selected in the runtime_. > -> - THE ABOVE VERSION IS OLD. NEEDS UPDATING. -> - The definition of specificity for dispatch candidates (including how it -> interacts with the subsumption relationship on typesets and the ordering of -> arguments). +> - Always prefer a member function for both `x.f y` and `f y x` notations. +> - Only member functions, current module's functions, and imported functions are +> considered to be in scope. Local variable `f` could not be used in the `x.f y` +> syntax. +> - Selecting the matching function: +> 1. Look up the member function. If it exists, select it. +> 2. If not, find all functions with the matching name in the current module and +> all directly imported modules. These functions are the _candidates_. +> 3. Eliminate any candidate `X` for which there is another candidate `Y` whose +> `this` argument type is strictly more specific. That is, `Y` this type is a +> substitution of `X` this type but not vice versa. +> 4. If not all of the remaining candidates have the same this type, the search +> fails. +> 5. Eliminate any candidate `X` for which there is another candidate `Y` which +> type signature is strictly more specific. That is, `Y` type signature is a +> substitution of `X` type signature. +> 6. If exactly one candidate remains, select it. Otherwise, the search fails. + +The runtime system of Enso identifies the type of a value in `obj.method_name` invocation. +It checks the _table of virtual methods_ for given type and finds proper +implementation of `method_name` to invoke. Should there be no method of given +name in the value's type (or its supertypes like `Any`) to invoke, +a `No_Such_Method` panic is raised. + +There is a special dispatch for [broken values & warnings](../semantics/errors.md). ## Multiple Dispatch Multiple dispatch is currently used for [binary operators](../syntax/functions.md#type-ascriptions-and-operator-resolution). -Supporting it for general functions remains an open question as to whether we -want to support proper multiple dispatch in Enso. Multiple dispatch refers to -the dynamic dispatch target being determined based not only on the type of the -`this` argument, but the types of the other arguments to the function. - -To do multiple dispatch properly, it is very important to get a rigorous -specification of the specificity algorithm. It must account for: - -- The typeset subsumption relationship. -- The ordering of arguments. -- How to handle defaulted and lazy arguments. -- Constraints in types. This means that for two candidates `f` and `g`, being - dispatched on a type `t` with constraint `c`, the more specific candidate is - the one that explicitly matches the constraints. An example follows: - - ```ruby - type HasName - name : String - - greet : t -> Nothing in IO - greet _ = print "I have no name!" - - greet : (t : HasName) -> Nothing in IO - greet t = print 'Hi, my name is `t.name`!' - - type Person - Pers (name : String) - - main = - p1 = Person.Pers "Joe" - greet p1 # Hi, my name is Joe! - greet 7 # I have no name - ``` +Multiple dispatch is also used on `from` conversions, because in +expression `T.from x` the function to use is based on both `T` and `x`. - Here, because `Person` conforms to the `HasName` interface, the second `greet` - implementation is chosen because the constraints make it more specific. +> [!WARNING] +> Supporting general _multiple dispatch is unlikely_ +> +> Supporting it for general functions remains an open question as to whether we +> want to support proper multiple dispatch in Enso. Multiple dispatch refers to +> the dynamic dispatch target being determined based not only on the type of the +> `this` argument, but the types of the other arguments to the function. +> +> To do multiple dispatch properly, it is very important to get a rigorous +> specification of the specificity algorithm. It must account for: +> +> - The typeset subsumption relationship. +> - The ordering of arguments. +> - How to handle defaulted and lazy arguments. +> - Constraints in types. This means that for two candidates `f` and `g`, being +> dispatched on a type `t` with constraint `c`, the more specific candidate is +> the one that explicitly matches the constraints. An example follows: +> +> ```ruby +> type HasName +> name : String +> +> greet : t -> Nothing in IO +> greet _ = print "I have no name!" +> +> greet : (t : HasName) -> Nothing in IO +> greet t = print 'Hi, my name is `t.name`!' +> +> type Person +> Pers (name : String) +> +> main = +> p1 = Person.Pers "Joe" +> greet p1 # Hi, my name is Joe! +> greet 7 # I have no name +> ``` +> +> Here, because `Person` conforms to the `HasName` interface, the second `greet` +> implementation is chosen because the constraints make it more specific. diff --git a/docs/types/errors.md b/docs/types/errors.md index 6bbbdb6bf2ef..1b38f4b38add 100644 --- a/docs/types/errors.md +++ b/docs/types/errors.md @@ -8,10 +8,11 @@ order: 12 # Errors -Enso supports two notions of errors. One is the standard asynchronous exceptions +Enso supports two notions of errors. One is the standard exceptions model, while the other is a theory of 'broken values' that propagate through computations. +> [!WARNING] > The actionables for this section are: > > - Greatly expand on the reasoning and theory behind the two exception models. @@ -27,14 +28,16 @@ computations. ## Async Exceptions +> [!WARNING] > The actionables for this section are: > +> - why is this called _"asynchronous"_ when the `Panic` is raised synchronously? > - Formalise the model of async exceptions as implemented. ## Broken Values In Enso we have the notion of a 'broken' value: one which is in an invalid state -but not an asynchronous error. While these may initially seem a touch useless, +but not an error. While these may initially seem a touch useless, they are actually key for the display of errors in the GUI. Broken values can be thought of like checked monadic exceptions in Haskell, but @@ -61,6 +64,7 @@ with an automatic propagation mechanism: - This allows for very natural error handling in the GUI. +> [!WARNING] > The actionables for this section are: > > - Determine what kinds of APIs we want to use async exceptions for, and which diff --git a/docs/types/evaluation.md b/docs/types/evaluation.md index 772cb77af188..6e45a3b4204f 100644 --- a/docs/types/evaluation.md +++ b/docs/types/evaluation.md @@ -12,19 +12,37 @@ Enso is a language that has strict semantics by default, but it can still be very useful to be able to opt-in to suspended computations (thunks) for the design of certain APIs. -To that end, Enso provides a mechanism for this through the type system. The -standard library defines a `Suspend a` type which, when used in explicit type -signatures, will cause the corresponding expression to be suspended. - -- The explicit calls to `Suspend` and `force` are inserted automatically by the - compiler doing demand analysis. -- This demand analysis process will also ensure that there are not polynomial - chains of suspend and force being inserted to ensure performance. +To that end, Enso provides a mechanism for this through the type system. +> [!WARNING] +> Enso is using `~` and `...` to defer computations and perform them lazily +> when needed. +> +> The +> standard library defines a `Suspend a` type which, when used in explicit type +> signatures, will cause the corresponding expression to be suspended. +> +> - The explicit calls to `Suspend` and `force` are inserted automatically by the +> compiler doing demand analysis. +> - This demand analysis process will also ensure that there are not polynomial +> chains of suspend and force being inserted to ensure performance. +> > The actionables for this section are as follows: > > - Specify this much better. +A function argument can be prefixed by `~`. That instructs the Enso runtime +system to provide such an arguments a thunk - a function to be evaluated later. +Such a thunk function is they evaluated when the value of the argument +is accessed/used. Such an evaluation is performed every time the argument value +is used. + +An atom argument can be prefixed by `~`. That instructs the Enso runtime system +to defer evaluation of the argument until it is first accessed. Then its thunk +is evaluated and when the evaluation is over, the atom argument value is replaced +by the computed value. Subsequent access to the atom argument will then use +the already evaluated value. + - [Specifying Suspension in the Type System](#specifying-suspension-in-the-type-system) @@ -33,7 +51,11 @@ signatures, will cause the corresponding expression to be suspended. ## Specifying Suspension in the Type System +> [!WARNING] > The actionables for this section are: > > - Actually specify how the type system interacts with eager and lazy > evaluation. + +Just use `~` to mark lazily computed function or atom arguments. The rest is handled +by the Enso runtime system. diff --git a/docs/types/function-types.md b/docs/types/function-types.md index 53c26f217e86..0d06a187eaab 100644 --- a/docs/types/function-types.md +++ b/docs/types/function-types.md @@ -11,6 +11,7 @@ order: 3 As a functional programming language, the type of functions in Enso (`->`) is key. There are a few things that should be noted about functions in Enso. +> [!NOTE] > The actionables for this section: > > - Work out a full specification for function typing and behaviour. @@ -47,60 +48,62 @@ Scope lookup proceeds from the function body outwards, as is standard for lexical scoping. For a detailed discussion of scoping, please see [the scoping documentation](../semantics/scoping.md). -## Structural Type Shorthand - -In Enso, we want to be able to write a type-signature that represents types in -terms of the operations that take place on the input values. A classical example -is `add`: - -```ruby -add : a -> b -> b + a -add = a -> b -> b + a -``` - -There are a few things to note about this signature from a design standpoint: - -- `a` and `b` are not the same type. This may, at first glance, seem like a - signature that can't work, but the return type, in combination with our - integrated `Convertible` mechanism gives us the tools to make it work. -- The return type is `a + b`. This is a shorthand expression for a detailed - desugaring. The desugaring provided below is what the typechecker would infer - based on such a signature. - -```ruby -add : forall a b c d. ({+ : Convertible b c => a -> c -> d} <: a) => a -> b -> d -``` - -This may look fairly strange at first, but we can work through the process as -follows: - -1. The expression `b + a` is syntactic sugar for a method call on a: `a.+ b`. -2. This means that there must be a `+` method on a that takes both an `a` and a - `b`, with return-type unspecified as of yet: `+ : a -> b -> ?` -3. However, as `Convertible` is built into the language, we have to consider - that for `a.+ b` to work, the `+` method can actually take any type to which - `b` converts. This introduces the constraint `Convertible b c`, and we get - `+ : a -> c -> ?` -4. The return type from a function need not be determined by its arguments, so - hence in the general case we have to default to an unrestricted type variable - giving `+ a -> c -> d`. -5. This method must exist on the type `a`, resulting in the constraint that the - row `{+ : a -> c -> d} <: a` must conform to that interface. -6. We now know the return type of `a + b`, and can rewrite it in the signature - as `d`. - -Please note that `a <: b` (which can be flipped as `:>`) means that `a` is a row -that is a sub-row contained within the row `b`. The containment relation allows -for the possibility that `a == b`. - -The inferred type for any function should, in general, match the given type -signature. Cases where this break down should only exist where the type -signature acts to constrain the function type further than would be inferred. - -> The actionables for this section are: +> [!WARNING] > > PLEASE NOTE. THIS IS OUT OF DATE. > +> ## Structural Type Shorthand +> +> In Enso, we want to be able to write a type-signature that represents types in +> terms of the operations that take place on the input values. A classical example +> is `add`: +> +> ```ruby +> add : a -> b -> b + a +> add = a -> b -> b + a +> ``` +> +> There are a few things to note about this signature from a design standpoint: +> +> - `a` and `b` are not the same type. This may, at first glance, seem like a +> signature that can't work, but the return type, in combination with our +> integrated `Convertible` mechanism gives us the tools to make it work. +> - The return type is `a + b`. This is a shorthand expression for a detailed +> desugaring. The desugaring provided below is what the typechecker would infer +> based on such a signature. +> +> ```ruby +> add : forall a b c d. ({+ : Convertible b c => a -> c -> d} <: a) => a -> b -> d +> ``` +> +> This may look fairly strange at first, but we can work through the process as +> follows: +> +> 1. The expression `b + a` is syntactic sugar for a method call on a: `a.+ b`. +> 2. This means that there must be a `+` method on a that takes both an `a` and a +> `b`, with return-type unspecified as of yet: `+ : a -> b -> ?` +> 3. However, as `Convertible` is built into the language, we have to consider +> that for `a.+ b` to work, the `+` method can actually take any type to which +> `b` converts. This introduces the constraint `Convertible b c`, and we get +> `+ : a -> c -> ?` +> 4. The return type from a function need not be determined by its arguments, so +> hence in the general case we have to default to an unrestricted type variable +> giving `+ a -> c -> d`. +> 5. This method must exist on the type `a`, resulting in the constraint that the +> row `{+ : a -> c -> d} <: a` must conform to that interface. +> 6. We now know the return type of `a + b`, and can rewrite it in the signature +> as `d`. +> +> Please note that `a <: b` (which can be flipped as `:>`) means that `a` is a row +> that is a sub-row contained within the row `b`. The containment relation allows +> for the possibility that `a == b`. +> +> The inferred type for any function should, in general, match the given type +> signature. Cases where this break down should only exist where the type +> signature acts to constrain the function type further than would be inferred. +> +> The actionables for this section are: +> > - Clean it up and work out how it applies in light of the new developments of > typesets. @@ -112,15 +115,26 @@ all arguments have been applied. This operator is `>>` (and its backwards cousin arguments, and the result consumes `n` arguments, applies them to `f`, and then applies the result of that plus any additional arguments to `g`. -```ruby -computeCoeff = (+) >> (*5) - -doThing = (+) >> (*) -``` +> [!WARNING] +> Enso does support `>>` as well as `<<` operators, but +> +> ```ruby +> computeCoeff = (+) >> (*5) +> doThing = (+) >> (*) +> +> main = computeCoeff 7 3 +> Execution finished with an error: Method `*` of comp.computeCoeff.f[comp.enso:11-12] a=7 b=_ could not be found. +> at comp.computeCoeff.g(comp.enso:14:9-11) +> at Function.>>(Function.enso:66:7-12) +> at comp.main(comp.enso:17:8-20) +> +> +> ``` In addition, we have the operator `.`, which acts as standard forward function chaining in Enso, and its backwards chaining cousin `<|`. +> [!NOTE] > The actionables from this section are: > > - Examples for the more advanced use-cases of `>>` to decide if the type diff --git a/docs/types/goals.md b/docs/types/goals.md index 37734129577b..11b53d69b584 100644 --- a/docs/types/goals.md +++ b/docs/types/goals.md @@ -23,13 +23,37 @@ needs to be as unobtrusive as possible. The high-level goals for the Enso type system are as follows: -- Inference should have maximal power. We want users to be _forced_ to write - type annotations in as few situations as possible. This means that, ideally, - we are able to infer higher-rank types and make impredicative instantiations - without annotations. -- Error messages must be informative. This is usually down to the details of the - implementation, but we'd rather not employ an algorithm that discards - contextual information that would be useful for crafting useful errors. -- Our aim is to create a powerful type system to support development, rather - than turn Enso into a research language. We want users to be able to add - safety gradually. +> [!WARNING] +> _Not a goal anymore_: Enso is a dynamic language. Static type +> inference is _not needed for execution_. As such _static typing_ is an +> optional component - more a _linter_ than essential part of the system. +> +> Inference should have maximal power. We want users to be _forced_ to write +> type annotations in as few situations as possible. This means that, ideally, +> we are able to infer higher-rank types and make impredicative instantiations +> without annotations. + +#### Error messages must be informative + +Clear error messages are essential for figuring out what the user needs to +change in own program to eliminate the error. This is true for both: + +- the runtime type errors +- the lints provided by _static type checker_ + +Ideally a type error shall contain proper identification of the error +origin/location and clear indication of what shall be changed to eliminate it. + +#### Early Runtime Type Errors + +Type checks shall be performed at the _"library boundary"_ rather than somewhere +deep inside of library code. Only then the user can under the context of the +error. + +#### Powerful Enough Type System + +Enso aim is to provide a powerful _enough_ type system to support development +done by _non-technical audience_. The type system shouldn't require master +degree in computer science to be used properly. As such the types are fully +optional and can be added gradually - usually only when a sample project is +turned into a reusable library. diff --git a/docs/types/hierarchy.md b/docs/types/hierarchy.md index 9b119bec5921..b0f76a383623 100644 --- a/docs/types/hierarchy.md +++ b/docs/types/hierarchy.md @@ -8,168 +8,122 @@ order: 2 # The Enso Type Hierarchy -Enso is a statically typed language based upon a theory of set-based typing, -what we call `typesets`. This is a novel approach, and it is key to our intent -for Enso to _feel_ like a dynamic language while still bringing enhanced safety. - - - -- [Typeset Theory](#typeset-theory) -- [Atoms](#atoms) -- [Typesets](#typesets) - - [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) - - [Scoping in Type Ascription](#scoping-in-type-ascription) -- [Projections](#projections) - - [Special Fields](#special-fields) - - - -## Typeset Theory - -- All types are denoted by a set of constructors, which represent the atomic - values of that type. We call these 'atoms'. For example, the typeset `Nat` is - made up of the atoms `1, 2, 3, ...` and so on. -- Constructors are grouped into typesets. -- These typesets are arranged into a modular lattice: - - The type `Any` is the typeset of all typesets. - - The type `Void` is the empty typeset. - - All atoms are typesets, but not all typesets are atoms. - - This lattice is ordered using the `<:` subsumption judgement. For more - information please see [typeset subsumption](#typeset-subsumption). - -All in all, this means that a value in Enso can have myriad different types -attributed to it, even though these may vary greatly in the level of -specificity. - -```ruby -7 : 7 : Natural : Integer : Number : Any : Any : ... -``` - -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 - a fresh name or a name already in scope, capitalisation is used to determine - which is meant. -- An uncapitalised identifier is assumed to be fresh, while a capitalised - identifier is assumed to be in scope. +Enso is a dynamic language, yet _every object_ in the running system _has a +type_. Type defines the set of operations that can be performed on a value. The +most generic type is `Any`. If a value has no better (more specific) type, it +has the type `Any`. All operations defined on type `Any` can be performed on any +value in the system. + +> [!WARNING] +> _Typeset theory is far from current state of affairs_: +> +> Enso is a statically typed language based upon a theory of set-based typing, +> what we call `typesets`. This is a novel approach, and it is key to our intent +> for Enso to _feel_ like a dynamic language while still bringing enhanced +> safety. +> +> ## Typeset Theory +> +> - All types are denoted by a set of constructors, which represent the atomic +> values of that type. We call these 'atoms'. For example, the typeset `Nat` +> is made up of the atoms `1, 2, 3, ...` and so on. +> - Constructors are grouped into typesets. +> - These typesets are arranged into a modular lattice: +> - The type `Any` is the typeset of all typesets. +> - The type `Void` is the empty typeset. +> - All atoms are typesets, but not all typesets are atoms. +> - This lattice is ordered using the `<:` subsumption judgement. For more +> information please see [typeset subsumption](#typeset-subsumption). + +A value in Enso can have multiple different types attributed to it. It is +possible to query/inspect these types during runtime and thus decide what +operations are available for a particular value at hand. + +> [!WARNING] +> _Probably not true in current system at all_ +> +> 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 a fresh name or a name already in scope, capitalisation is used to +> determine which is meant. +> - An uncapitalised identifier is assumed to be fresh, while a capitalised +> identifier is assumed to be in scope. ## Atoms Atoms are the fundamental building blocks of types in Enso, so named because -they are small units of 'type', but nonetheless may be separated further. In -Enso's type hierarchy, atoms are the typesets that are unified _nominally_, -meaning that every atom has a discrete identity. +they are small units of 'type', but nonetheless may be separated further. When +defining a `type` in Enso, one can associate to it multiple _atom constructors_. +Such constructors are then used to create instances of the `type`. - Atoms can be thought of as the 'values' of Enso's type system. Formally an atom is a product type with named fields, where the fields are polymorphic. -- Atoms have _unique identity_. This means that while a typeset may subsume an - atom, an atom can never be subsumed by another atom, even if it has the same - number of fields with the same names. -- An atom, thus, can only unify with a site expecting that atom, or some - anonymous typeset. +- Atoms have _unique identity_. This means an atom has a particular type, + however an atom can never be a type of another atom. +- An atom, thus, can only unify with a site expecting that atom, or its type or + the general type `Any`. -The following are all examples of atoms with a usage example: - -```ruby -type Nothing -type Just value -atom Vec3 x y z -atom Vec2 x y - -v = V3 1 2 3 : V3 1 2 3 : V3 Int Int Int : V3 Any Any Any : Any -``` - -## Typesets - -Typesets in Enso are an entity unique to Enso's type system. They are a -fundamental recognition of types as 'sets of values' in Enso, and while they -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 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. - -- 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). 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. - -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: +The following defines a type `Option` with two atoms `None` and `Some`: ```ruby type Maybe a Nothing - type Just (value : a) + Just (value : a) isJust = case this of Nothing -> False Just _ -> True nothing = not isJust -``` +v = Maybe.Just "Hi" -Becomes +# value `v` has type `Maybe`: +v:Maybe -```ruby -atom Just value -maybe a = - { (Nothing | Just a), isJust: IsJust = isJust, nothing : Nothing = nothing } - -Nothing.isJust : Maybe a -> Bool -Nothing.isJust this = case this of - Nothing -> False - Just _ -> True - -Just.isJust : Maybe a -> Bool -Just.isJust this = case this of - Nothing -> False - Just _ -> True - -Nothing.nothing : Maybe a -> Bool -Nothing.nothing = not isJust - -Just.nothing : Maybe a -> Bool -Just.nothing = not isJust +# `v.value` has type `Text`: +v.value:Text ``` -> The actionables for this section are as follows: +> [!WARNING] +> There are no _Typesets_ in Enso anymore +> +> Typesets in Enso are an entity unique to Enso's type system. They are a +> fundamental recognition of types as 'sets of values' in Enso, and while they +> share some similarities with records they are a far more general notion. > -> - 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). +> - 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 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. +> +> - 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). 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 `;`. + +Types can be combined using the [typeset operators](#typeset-operators) defined +below. ### Typeset Operators -Enso defines a set of operations on typesets that can be used to combine and +Enso defines a set of operations on types that can be used to combine and manipulate them. Any use of these operators introduces typing evidence which may later be discharged through pattern matching. @@ -177,30 +131,36 @@ They are as follows: - **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). +- **Context Ascription - `in`:** This operator ascribes the monadic context + given by its right operand to the expression of its left operand. - **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. +> [!WARNING] +> These operators _don't seem to be supported_. There is no plan to +> support following operators now: +> +> - **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. + 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. +> [!NOTE] > The actionables for this section are: > > - When necessary, we need to _explicitly formalise_ the semantics of all of @@ -209,50 +169,52 @@ design documentation. > 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 -the notation `a <: b`) if the following hold recursively. This can be thought of -as a 'can behave as' relation. - -1. `a` contains a subset of the labels in `b`. It should be noted that `a` is - not _limited to_ being a subset of the labels in `b`. -2. For each label in `a`, the type of that label `t` is subsumed by the type - `q` of the corresponding label in `b`. That is, `t <: q`, defined as - follows: - - 1. If both `t` and `q` are atoms, then it holds only if `t` and `q` are the - same atom (have the same identity). - 2. If `t` is an atom, then it holds only if the fields in `t` are subsumed - by `q`. - 3. If either `t` or `q` is a function type but not _both_ `t` and q are - function types, then the relation does not hold. - 4. If both `t` and `q` are function types, then the relation holds if: - - - If `t` contains defaulted arguments, not present in `q`, then these - can be ignored for the purposes of determining whether `t <: q`. For - example, `f : a -> b = x -> c` is subsumed by `f : a -> c`. - - For the _argument_ position of both `t` and `q`, `t.arg <: q.arg` (the - argument position is covariant). - - For the _return_ position of both `t` and `q`, if it is not a function - type, then `t.ret <: q.ret` (the return position is covariant). If it - is a function type then recurse. - - 5. If the types have constraints then the constraints must match. A - constraint is simply an application of the `<:` relation. - 6. The types both have the same relevance and visibility (in the dependent - sense). - -3. For any typeset `a`, the relation `a <: Any` always holds, and the converse - `Any <: a` never holds. -4. For any typeset `a`, the relation `a <: Void` never holds, and the converse - `Void <: a` always holds. - -Two typesets `A` and `B` are defined to be structurally equal if `A <: B` and -`B <: A`. +> [!WARNING] +> _Typeset Subsumption_ isn't relevant +> +> For two typesets `a` and `b`, `a` is said to be subsumed by `b` (written using +> the notation `a <: b`) if the following hold recursively. This can be thought +> of as a 'can behave as' relation. +> +> 1. `a` contains a subset of the labels in `b`. It should be noted that `a` is +> not _limited to_ being a subset of the labels in `b`. +> 2. For each label in `a`, the type of that label `t` is subsumed by the type +> `q` of the corresponding label in `b`. That is, `t <: q`, defined as +> follows: +> +> 1. If both `t` and `q` are atoms, then it holds only if `t` and `q` are +> the same atom (have the same identity). +> 2. If `t` is an atom, then it holds only if the fields in `t` are +> subsumed by `q`. +> 3. If either `t` or `q` is a function type but not _both_ `t` and q are +> function types, then the relation does not hold. +> 4. If both `t` and `q` are function types, then the relation holds if: +> +> - If `t` contains defaulted arguments, not present in `q`, then these +> can be ignored for the purposes of determining whether `t <: q`. For +> example, `f : a -> b = x -> c` is subsumed by `f : a -> c`. +> - For the _argument_ position of both `t` and `q`, `t.arg <: q.arg` +> (the argument position is covariant). +> - For the _return_ position of both `t` and `q`, if it is not a +> function type, then `t.ret <: q.ret` (the return position is +> covariant). If it is a function type then recurse. +> +> 5. If the types have constraints then the constraints must match. A +> constraint is simply an application of the `<:` relation. +> 6. The types both have the same relevance and visibility (in the +> dependent sense). +> +> 3. For any typeset `a`, the relation `a <: Any` always holds, and the +> converse `Any <: a` never holds. +> 4. For any typeset `a`, the relation `a <: Void` never holds, and the +> converse `Void <: a` always holds. +> +> Two typesets `A` and `B` are defined to be structurally equal if `A <: B` and +> `B <: A`. > The actionables for this section are as follows: > +> - Just _delete it_!? > - Fix the above. It isn't 100% correct, but should convey a general gist. Use > examples including all the operators. > - Ensure that co- and contra-variance are handled properly. They are a bit odd @@ -270,259 +232,113 @@ Two typesets `A` and `B` are defined to be structurally equal if `A <: B` and > without subtyping. Conventionally we wouldn't be able to, but with our > theory we may. -### Unsafe Typeset Field Mutation +### Field Mutation For performance it is sometimes necessary to have the ability to _directly_ -_mutate_ the field of a typeset. This is most often necessary for atoms -themselves, but as atoms are typesets this also applies. - -- We define a method `setField : (field : Name) -> (value : Any) -> Nothing` - that performs in-place field mutation of the field `field` to set its value to - `any`. -- 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. +_mutate_ the field of an atom. This is possible using `Meta.atom_with_hole`. +Such a mutation can happen _only once_. ## 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 -the relation `i <: t` (as in [typeset subsumption](#typeset-subsumption)) -holding. - -This means that types need not _explicitly_ implement interfaces, which can be -thought of as a form of static duck typing. However, when defining a new type, -users may choose to explicitly state that it defines an interface. This has two -main benefits: - -- We can include default implementations from the interface definition. -- We can provide better diagnostics in the compiler as we can point to the - definition site instead of the use site. - -```ruby -type HasName - name: String - name = "unnamed" - -type Vector a - this: HasName - V2 x:a y:a - V3 x:a y:a z:a +Historically interfaces used to be defined by _duck typing_. As Enso is a +dynamic language, having two types with the same operations means they can be +used interchangingly. -name (this:Int) = "IntName" +> [!NOTE] +> A work on [type classes](https://github.com/orgs/enso-org/discussions/11366) support is under way -greet (t:HasName) = print 'Hi, my name is `t.name`' - -main = - greet (V3 1 2 3) - greet 8 -``` - -As an aside, it should be noted that the nature of Enso's typesets means that it -is easy to express far more general interfaces than Haskell's typeclasses can. +> [!WARNING] +> _Doesn't match reality:_ +> +> 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 +> the relation `i <: t` (as in [typeset subsumption](#typeset-subsumption)) +> holding. +> +> This means that types need not _explicitly_ implement interfaces, which can be +> thought of as a form of static duck typing. However, when defining a new type, +> users may choose to explicitly state that it defines an interface. This has +> two main benefits: +> +> - We can include default implementations from the interface definition. +> - We can provide better diagnostics in the compiler as we can point to the +> definition site instead of the use site. +> +> ```ruby +> type HasName +> name: String +> name = "unnamed" +> +> type Vector a +> this: HasName +> V2 x:a y:a +> V3 x:a y:a z:a +> +> name (this:Int) = "IntName" +> +> greet (t:HasName) = print 'Hi, my name is `t.name`' +> +> main = +> greet (V3 1 2 3) +> greet 8 +> ``` +> +> As an aside, it should be noted that the nature of Enso's typesets means that +> it is easy to express far more general interfaces than Haskell's typeclasses +> can. -### Special Interfaces + -It should be noted, however, that a type that implements an explicit `destroy` -method should still implement explicit methods for resource handling as lexical -lifetimes are not always sufficient (e.g. a socket that you may want to close -and re-open in the same block). - -> The actionables for this section are: -> -> - Determine how this interacts with copying and moving. +To control lifecycle of a value use `Managed_Resource` and its support for +_finalizers_. ## Type Ascription -Like all statically-typed programming languages, Enso provides the means for the -user to ascribe a type to a value. In Enso, this is done using the `:` operator. An expression `a : b` says that the expression denoted by `a` has the type -denoted by the expression `b`. However, unlike in many programming languages, -the types ascribed to values in Enso are not the be-all and end-all. - -- The Enso compiler is free to infer a _more specific_ type than the one - provided in a type signature. If this is the case, then the actual type of the - value is the inferred type rather than the provided type. - - ```ruby - a = 17 : Int | Text - b = a + 1 # This is not an error - ``` - -- If the Enso compiler would infer a _more general_ type than the one provided - in a type signature, then the signature _constrains_ the allowable type of the - value. -- Type signatures must be subsumed by the inferred type of the value, otherwise - the compiler will raise an error. This includes - -### Scoping in Type Ascription - -Enso intends to support some form of mutual scoping between the left and right -sides of the type ascription operator. This introduces some complexity into the -typechecker but brings some significant benefits. - -- It is common in dependently-typed languages for the signature to balloon - significantly as you add more constraints to your program. -- To this end, Enso wants to support a sharing of scopes between the top-level - scope of the type signature's right-hand-side, and the top-level scope of the - signature's left hand side. -- This will allow users to move complexity _out_ of the type signature and into - the body of the expression, aiding code clarity. -- It does, however, introduce some significant complexity around recursive - bindings in groups, and the desugaring needs to depend on combinations of - `>>=` and `fix`. - -## Projections - -In order to work efficiently with typesets, we need the ability to seamlessly -access and modify (immutably) their properties. In the context of our type -theory, this functionality is known as a _projection_, in that it projects a -value from (or into) a typeset. - -Coming from Haskell, we are well-versed with the flexibility of lenses, and more -generally _optics_. To that end, we base our projection operations on standard -theories of optics. While we _do_ need to formalise this, for now we provide -examples of the expected basic usage. This only covers lenses, while in the -future we will likely want prisms and other more-advanced optics. - -A projection is generated for each field of a typeset. +denoted by the expression `b`. +> [!WARNING] +> No support for Scoping in Type Ascription +> +> Enso intends to support some form of mutual scoping between the left and right +> sides of the type ascription operator. This introduces some complexity into +> the typechecker but brings some significant benefits. +> +> - It is common in dependently-typed languages for the signature to balloon +> significantly as you add more constraints to your program. +> - To this end, Enso wants to support a sharing of scopes between the top-level +> scope of the type signature's right-hand-side, and the top-level scope of +> the signature's left hand side. +> - This will allow users to move complexity _out_ of the type signature and +> into the body of the expression, aiding code clarity. +> - It does, however, introduce some significant complexity around recursive +> bindings in groups, and the desugaring needs to depend on combinations of +> `>>=` and `fix`. + +> [!WARNING] +> There are _no projections_ right now and none are planned +> +> In order to work efficiently with typesets, we need the ability to seamlessly +> access and modify (immutably) their properties. In the context of our type +> theory, this functionality is known as a _projection_, in that it projects a +> value from (or into) a typeset. +> +> Coming from Haskell, we are well-versed with the flexibility of lenses, and +> more generally _optics_. To that end, we base our projection operations on +> standard theories of optics. While we _do_ need to formalise this, for now we +> provide examples of the expected basic usage. This only covers lenses, while +> in the future we will likely want prisms and other more-advanced optics. +> +> A projection is generated for each field of a typeset. +> > Actionables for this section: > > - Work out whether standard optics theory with custom types is sufficient for @@ -531,12 +347,12 @@ A projection is generated for each field of a typeset. > are likely to be a lot of edge-cases, so it's important that we make sure we > know how to get as much of it working as possible. > - How (if at all) do lenses differ for atoms and typesets? - -### Special Fields - -We also define special projections from typesets: - -- `index`: The expression `t.n`, where `n` is of type `Number` is translated to - `t.index n`. -- `field`: The expression `t.s` where `s` is of type `Text` is translated to - `t.fieldByName s`. +> +> ### Special Fields +> +> We also define special projections from typesets: +> +> - `index`: The expression `t.n`, where `n` is of type `Number` is translated +> to `t.index n`. +> - `field`: The expression `t.s` where `s` is of type `Text` is translated to +> `t.fieldByName s`. diff --git a/docs/types/inference-and-checking.md b/docs/types/inference-and-checking.md index 09d739dbd17c..f2c877ab638e 100644 --- a/docs/types/inference-and-checking.md +++ b/docs/types/inference-and-checking.md @@ -8,11 +8,13 @@ order: 13 # Inference and Checking -As a statically-typed language, Enso is built with a sophisticated type checker -capable of reasoning about a fully dependently-typed system. However, a type +In spite of being dynamically-typed language, Enso is built with a sophisticated type checker +capable of reasoning about Enso typed system. However, a type checker on its own is quite useless. For Enso to truly be usable, it must also have a powerful type inference engine. +> [!WARNING] +> > The actionables for this section are: > > - Work out how on earth we do inference and how we maximise inference power. @@ -41,6 +43,7 @@ In order to make Enso's type inference as helpful and friendly as possible to our users, we want the ability to infer the _maximal subset_ of the types that Enso can express. +> [!WARNING] > The actionables for this section are: > > - How do we do inference for higher-rank and impredicative instantiations. @@ -56,18 +59,21 @@ Enso can express. ## Type Inference Algorithm +> [!WARNING] > The actionables for this section are: > > - Specify the inference algorithm. ### Inferring Dependency +> [!WARNING] > The actionables for this section are: > > - Specify how (if at all) we can infer dependent quantifiers. ## Type Checking Algorithm +> [!WARNING] > The actionables for this section are: > > - Specify the type checking algorithm. diff --git a/docs/types/modules.md b/docs/types/modules.md index 736bc6b8bf22..564caff5da0b 100644 --- a/docs/types/modules.md +++ b/docs/types/modules.md @@ -11,7 +11,7 @@ order: 7 With such a flexible type system in Enso, the need for making modules first-class is obviated. Instead, a module is very much its own entity, being simply a container for bindings (whether they be functions, methods, atoms, or -more generic typesets). +types). > The actionables for this section are: > @@ -26,15 +26,22 @@ more generic typesets). ## Resolving Name Clashes -Enso modules employ the following rules in order to avoid name clashes: - -- Where the module name clashes with a member contained in the module, the - member is preferred. If you need the module you must import it qualified under - another name. -- We provide the alias `here` as a way to access the name of the current module. +> [!WARNING] +> There is no `here` keyword anymore and the clash resultion is probably also +> not working. +> +> Enso modules employ the following rules in order to avoid name clashes: +> +> - Where the module name clashes with a member contained in the module, the +> member is preferred. If you need the module you must import it qualified under +> another name. +> - We provide the alias `here` as a way to access the name of the current module. ## Scoping and Imports +> [!WARNING] +> Review by an _imports expert_ is needed! + To use the contents of a module we need a way to bring them into scope. Like most languages, Enso provides an _import_ mechanism for this. Enso has four different kinds of imports that may be combined freely, all of which take a diff --git a/docs/types/parallelism.md b/docs/types/parallelism.md index 5f588c0f00e1..4c4930f75961 100644 --- a/docs/types/parallelism.md +++ b/docs/types/parallelism.md @@ -21,12 +21,14 @@ by the compiler to automatically parallelise some sections of Enso programs. ## Supporting Parallelism Analysis with Types +> [!WARNING] > The actionables for this section are: > > - Work out how the type checker can support parallelism analysis. ## Constructs That Can Be Parallelised +> [!WARNING] > The actionables for this section are: > > - Provide an analysis of the language constructs that could automatically be diff --git a/docs/types/pattern-matching.md b/docs/types/pattern-matching.md index 4366e2565373..5580b6e5c28f 100644 --- a/docs/types/pattern-matching.md +++ b/docs/types/pattern-matching.md @@ -8,19 +8,9 @@ order: 5 # Pattern Matching -Pattern matching in Enso works similarly to as you would expect in various other +Pattern matching in Enso follows typical operations promoted by various other functional languages. Typing information is _always_ refined in the branches of -a case expression, which interacts well with dependent typing and type-term -unification. - -> The actionables for this section : -> -> - How do we type pattern matching? -> - Exactly how (and what) evidence is discharged during matching? -> - How can we use bijective applications of the -> [typeset operators](/hierarchy.md#typeset-operators) to perform pattern -> matching? -> - How do we extend this to structural matching in general on typesets? +a case expression. @@ -33,18 +23,20 @@ unification. ## Positional Matching -Matching on the scrutinee by structure. This works both for atoms and typesets -(for typesets it is a subsumption judgement). +It is possible to match on the scrutinee by structure for an atom: ```ruby +from Standard.Base.IO import println + type Vector a V2 x:a y:a V3 x:a y:a z:a -v = Vector.V3 x y z +main = + v = Vector.V3 "a" "b" "c" -case v of - Vector.V3 x y z -> print x + case v of + Vector.V3 x _ _ -> println x ``` ## Type Matching @@ -53,19 +45,20 @@ Matching purely by the types involved, and not matching on structure. ```ruby case v of - Vector.V3 -> print v.x + v3:Vector -> print v3.x ``` -## Name Matching on Labels - -Matching on the labels defined within a type for both atoms and typesets, with -renaming. - -```ruby -case v of - Vector.V3 {x y} -> print x - {x} -> print x -``` +> [!WARNING] +> **Unsupported:** Name Matching on Labels +> +> Matching on the labels defined within a type for both atoms and typesets, with +> renaming. +> +> ```ruby +> case v of +> Vector.V3 {x y} -> print x +> {x} -> print x +> ``` ## Naming Scrutinees @@ -73,6 +66,10 @@ Ascribing a name of a scrutinee is done using the standard typing judgement. This works due to the type-term unification present in Enso. ```ruby -case _ of - v : Vector.V3 -> print v,x +v = Vector.V3 "a" "b" "c" + +f = case _ of + Vector.V3 x _ _ -> println x + +f v ``` diff --git a/docs/types/references.md b/docs/types/references.md index 5f092c79875b..7c2122217b07 100644 --- a/docs/types/references.md +++ b/docs/types/references.md @@ -8,6 +8,8 @@ order: 15 # References + + This file contains a variety of useful references for those wanting to understand the concepts and research that underlie Enso's type system and type theory. @@ -44,7 +46,7 @@ theory. ## Monadic Contexts -- [Supermonads](http://eprints.nottingham.ac.uk/36156/1/paper.pdf) +- [Supermonads](https://web.archive.org/web/20180719132706/http://eprints.nottingham.ac.uk/36156/1/paper.pdf) ## Refinement Typing and Compiler Assistance diff --git a/docs/types/type-directed-programming.md b/docs/types/type-directed-programming.md index cdb786b907fb..11e6027ed112 100644 --- a/docs/types/type-directed-programming.md +++ b/docs/types/type-directed-programming.md @@ -14,8 +14,10 @@ based on types. This is an _advanced_ feature and is not expected to be used by the novice, but it is nonetheless an important feature for working with a powerful type system. +> [!WARNING] > The actionables for this section are: > +> - Just _delete it all_!? > - Examine what other ways we can exploit type information to aid development. @@ -29,6 +31,7 @@ powerful type system. ## Typed Holes +> [!WARNING] > The actionables for this section are: > > - Determine how we want to support typed holes. @@ -36,6 +39,7 @@ powerful type system. ## Case Splitting +> [!WARNING] > The actionables for this section are: > > - Determine how we want to support case splitting. @@ -43,12 +47,14 @@ powerful type system. ## Row Manipulation +> [!WARNING] > The actionables for this section are: > > - Determine how we want to support row manipulation. ## Dependent Sum Manipulation +> [!WARNING] > The actionables for this section are: > > - Determine how we want to support dependent sum manipulation.