... | ... | @@ -99,10 +99,13 @@ would allow for even easier use of punned identifiers in pun-avoiding code. |
|
|
|
|
|
More generally, we advocate the following principle:
|
|
|
|
|
|
**Syntactic unification principle.** In the absence of punning, there is no difference
|
|
|
**Syntactic Unification Principle.** In the absence of punning, there is no difference
|
|
|
between type-syntax and term-syntax.
|
|
|
|
|
|
This principle means that a DH programmer who avoids punning can simply forget about the distinction
|
|
|
This is a *long term* goal: see [The Glorious Future](https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell#11-the-glorious-future) below. It is *not* true of Dependent Haskell as described here: type-syntax is, for now, a proper subset of term-syntax. We describe this further in [Dependent application and the Static Subset]().
|
|
|
However, from a *scoping* point of view, it is already true. Absent punning, you do not need to reason about term-syntax vs type-syntax when resolving scopes.
|
|
|
|
|
|
The Syntactic Unification Principle means that a DH programmer who avoids punning can (in the end) simply forget about the distinction
|
|
|
between type-syntax and term-syntax, and the context-sensitivity these notions require. This is meant
|
|
|
to be a simplification available to those programmers. As we design DH, this principle informs
|
|
|
design decisions, so that it may be true once DH is fully realized.
|
... | ... | @@ -265,7 +268,7 @@ only when in *checking* mode of bidirectional type-checking, never in *inference |
|
|
above, we do indeed know the result type: `Vec n a`. We can thus perform an informative pattern-match, as required
|
|
|
to accept the definition.
|
|
|
|
|
|
### 6. Dependent application
|
|
|
### 6. Dependent application and the Static Subset
|
|
|
|
|
|
Suppose we have a function `f :: foreach (a::ty) -> blah` or `f :: forall (a::ty) -> blah`. Then at a
|
|
|
call site the programmer must supply an explicit argument, so the call will look like
|
... | ... | |