Remove references to dependent types (#3217)

docs/enso-philosophy.md

@@ -24,8 +24,8 @@ From a technical point of view, Enso incorporates many of the recent innovations
 in the design and development of programming languages to improve the user
 experience. It provides higher-order functions, strict semantics with opt-in
 laziness, and opt-in algebraic data types, all under the auspices of a novel
-type system that merges dependent typing with a great user experience. Enso is
-the culmination of many years of research into functional programming languages,
+type system that merges gradual typing with a great user experience. Enso is the
+culmination of many years of research into functional programming languages,
 consolidating the work trail-blazed by Haskell, Idris and Agda, but also
 improvements in user-experience and ergonomics.
 

docs/polyglot/polyglot-bindings.md

@@ -87,7 +87,6 @@ We went the way of the variadic call for multiple reasons:
   subtyping and overloading).
 - It is flexible and easy to expand in the future.
 - We can easily build a more Enso-feeling interface on top of it.
-- It can still be typed due to our plans for dependent vector types.
 
 By way of illustrative example, Java supports method overloading and subtyping,
 two things which have no real equivalent in the Enso type system.

docs/types/README.md

@@ -19,8 +19,7 @@ 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, combined with dependent
-types.
+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
@@ -67,7 +66,5 @@ Information on the type system is broken up into the following sections:
   system.
 - [**Type Inference and Checking:**](./inference-and-checking.md) A description
   of Enso's type inference and checking system.
-- [**Dependent Typing:**](./dependent-typing.md) A description of the dependent
-  nature of Enso's type system.
 - [**References:**](./references.md) Useful references for working on the type
   system and its theory.

docs/types/dependent-typing.md

@@ -1,101 +0,0 @@
----
-layout: developer-doc
-title: Dependent Typing
-category: types
-tags: [types, inference, checking, dependent, dependency]
-order: 14
----
-
-# Dependent Typing
-
-Enso is a [dependently typed](https://en.wikipedia.org/wiki/Dependent_type)
-programming language. This means that types are first-class values in the
-language, and hence can be manipulated and computed upon just like any other
-value. To the same end, there is no distinction between types and kinds, meaning
-that Enso obeys the 'Type in Type' axiom of dependent types. While this does
-make the language unsound as a logic, the type safety properties do not depend
-on this fact.
-
-In essence, values are types and types are values, and all kinds are also types.
-This means that, in Enso, you can run _arbitrary_ code to compute with types.
-All in all, dependency in Enso is not about being a proof system, but is instead
-about enabling practical usage without hampering usability. To that end we
-combine a powerful and non-traditional dependently-typed system with the ability
-to automate much of the proof burden through SMT solvers.
-
-> The actionables for this section are:
->
-> - Do we want the ability to explicitly quantify type variables for visibility,
->   dependency, relevance and requiredness (forall, foreach, etc).
-> - How do we infer as much of these above properties as possible?
-> - Based on QTT and RAE's thesis.
-
-<!-- MarkdownTOC levels="2,3" autolink="true" -->
-
-- [Proving Program Properties](#proving-program-properties)
-- [Automating the Proof Burden](#automating-the-proof-burden)
-
-<!-- /MarkdownTOC -->
-
-## Proving Program Properties
-
-Some notes:
-
-- Dependent types as constructing proofs through combining types. Combining
-  types provides evidence which can be discharged to create a proof. A value can
-  then only be constructed by discharging a proof.
-- To provide more predictable inference in dependent contexts, this system will
-  draw on the notion of _matchability polymorphism_ as outlined in the
-  higher-order type-level programming paper. The key recognition to make,
-  however is that where that paper was required to deal with
-  backwards-compatibility concerns, we are not, and hence can generalise all
-  definitions to be matchability polymorphic where appropriate.
-- Provide some keyword (`prove`) to tell the compiler that a certain property
-  should hold when typechecking. It takes an unrestricted expression on types,
-  and utilises this when typechecking. It may also take a string description of
-  the property to prove, allowing for nicer error messages:
-
-  ```
-  append : (v1 : Vector a) -> (v2 : Vector a) -> (v3 : Vector a)
-  append = vec1 -> vec2 ->
-      prove (v3.size == v1.size + v2.size) "appending augments length"
-      ...
-  ```
-
-  Sample error:
-
-  ```
-  [line, col] Unable to prove that "appending augments length":
-      Required Property: v3.size == v1.size + v2.size
-      Proof State:       <state>
-
-      <caret diagnostics>
-  ```
-
-  This gives rise to the question as to how we determine which properties (or
-  data) are able to be reasoned about statically.
-
-- Dependent types in Enso will desugar to an application of Quantitative Type
-  Theory.
-
-> The actionables for this section are:
->
-> - Specify how we want dependency to behave in a _far more rigorous_ fashion.
-
-## Automating the Proof Burden
-
-Even with as capable and simple a dependently-typed system as that provided by
-Enso, there is still a burden of proof imposed on our users that want to use
-these features. However, the language [F\*](https://www.fstar-lang.org/) has
-pioneered the combination of a dependently-typed system with an SMT solver to
-allow the automation of many of the simpler proofs.
-
-- The Enso typechecker will integrate an aggressive proof rewrite engine to
-  automate as much of the proof burden as possible.
-
-> The actionables for this section are:
->
-> - What is the impact of wanting this on our underlying type theory?
-> - Where and how can we draw the boundary between manual and automated proof?
-> - How much re-writing can we do (as aggressive as possible) to assist the SMT
->   solver and remove as much proof burden as possible.

docs/types/goals.md

@@ -30,11 +30,6 @@ The high-level goals for the Enso type system are as follows:
 - 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.
-- Dependent types are a big boon for safety in programming languages, allowing
-  the users that _want to_ to express additional properties of their programs in
-  their types. We would like to introduce dependent types in future, but would
-  welcome insight on whether it is perhaps easier to do so from the get go. If
-  doing so, we would prefer to go with `Type : Type`.
 - 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.

docs/types/hierarchy.md

@@ -493,10 +493,6 @@ the types ascribed to values in Enso are not the be-all and end-all.
 - Type signatures must be subsumed by the inferred type of the value, otherwise
   the compiler will raise an error. This includes
 
-Additionally, as Enso is a dependently-typed language, the expression `b` may
-contain arbitrary Enso expressions. The type-checking of such signatures is
-discussed further in the section on [dependency](./dependent-typing.md).
-
 ### Scoping in Type Ascription
 
 Enso intends to support some form of mutual scoping between the left and right

docs/types/references.md

@@ -14,7 +14,6 @@ theory.
 
 <!-- MarkdownTOC levels="2,3" autolink="true" -->
 
-- [Dependent Types](#dependent-types)
 - [Gradual Typing](#gradual-typing)
 - [Maximum Inference Power](#maximum-inference-power)
 - [Monadic Contexts](#monadic-contexts)
@@ -25,24 +24,6 @@ theory.
 
 <!-- /MarkdownTOC -->
 
-## Dependent Types
-
-- [A Classical Sequent Calculus for Dependent Types](https://hal.inria.fr/hal-01519929/document)
-- [Dependent Information Flow Types](http://ctp.di.fct.unl.pt/~luisal/resources/popl15-paper187.pdf)
-- [Dependent Intersection: A New Way of Defining Records in Type Theory](https://ieeexplore.ieee.org/document/1210048)
-- [Dependent Types and Monadic Effects in F\*](https://www.fstar-lang.org/papers/mumon/)
-- [Dependent Types in Haskell: Theory and Practice](https://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf)
-- [Dynamic Typing with Dependent Types](https://link.springer.com/chapter/10.1007/1-4020-8141-3_34)
-- [Handling Delimited Continuations with Dependent Types](https://dl.acm.org/doi/10.1145/3236764)
-- [Integrating Linear and Dependent Types](https://www.cl.cam.ac.uk/~nk480/dlnl-paper.pdf)
-- [Irrelevance, Heterogeneous Equality, and Call-by-Value Dependent Type Systems](https://www.cis.upenn.edu/~sweirich/papers/msfp12prog.pdf)
-- [Lightweight Invariants with Full Dependent Types](https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.5717)
-- [Normnalisation through Evaluation for Sized Dependent Types](https://core.ac.uk/display/94336601)
-- [Practical Erasure in Dependently-Typed Languages](https://eb.host.cs.st-andrews.ac.uk/drafts/dtp-erasure-draft.pdf)
-- [Resourceful Dependent Types](http://www.cse.chalmers.se/~abela/types18.pdf)
-- [Syntax and Semantics of Quantitative Type Theory](https://bentnib.org/quantitative-type-theory.pdf)
-- [Verifying Higher-Order Programs with the Dijkstra Monad](https://www.microsoft.com/en-us/research/publication/verifying-higher-order-programs-with-the-dijkstra-monad/)
-
 ## Gradual Typing
 
 - [Approximate Normalisation for Gradual Dependent Types](https://arxiv.org/abs/1906.06469)