Useful but limited polymorphism
This commit is contained in:
@@ -94,7 +94,110 @@ view envelope is well-formed, and recursively validates the `baseView`, but it
|
||||
must treat the guard payload/reference as opaque executable data, not as another
|
||||
View.
|
||||
|
||||
## 4. Guards
|
||||
## 4. Polymorphic and Abstract Views
|
||||
|
||||
View Contracts support portable polymorphism over Views. The View language is
|
||||
interpreted by the same portable checker model implemented in `tricu` terms.
|
||||
|
||||
Source syntax may use underscore-prefixed names as View variables inside
|
||||
annotations:
|
||||
|
||||
```tri
|
||||
id x@_a =@_a x
|
||||
const x@_a y@_b =@_a x
|
||||
compose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)
|
||||
```
|
||||
|
||||
In the portable artifact, these lower to scoped View binders rather than
|
||||
unscoped source-name conventions. This fits the existing View encoding style:
|
||||
Views are tagged records with numeric tags and tagged fields. Polymorphic forms
|
||||
are View records such as:
|
||||
|
||||
```text
|
||||
Var localId
|
||||
Forall binders body
|
||||
Exists binders body
|
||||
```
|
||||
|
||||
The current durable encoding uses stable local binder IDs. For example,
|
||||
`id x@_a =@_a x` exports a shape equivalent to:
|
||||
|
||||
```text
|
||||
Forall [0] (Fn [Var 0] (Var 0))
|
||||
```
|
||||
|
||||
Source names like `_a` are for authoring; the artifact carries binder scope and
|
||||
local IDs rather than relying on source-name identity.
|
||||
|
||||
`Forall` supports generic contracts:
|
||||
|
||||
```tri
|
||||
map f@(Fn [_a] _b) xs@(List _a) =@(List _b) ...
|
||||
head xs@(NonEmptyList _a) =@_a ...
|
||||
```
|
||||
|
||||
At each checked use, the checker instantiates quantified variables into
|
||||
use-local internal variables and solves View compatibility constraints. The
|
||||
portable checker uses structural use-local IDs rather than expensive numeric
|
||||
freshening, and treats unconstrained variable-variable matches as constraints
|
||||
that do not create substitution cycles. Concrete observations still bind these
|
||||
variables when enough information is available. This is what lets explicitly
|
||||
annotated higher-order boundaries accept polymorphic values, for example
|
||||
`compose id id "x"`, and lets quantified values satisfy concrete requirements
|
||||
such as `Fn [String] String`. It gives useful polymorphic contracts for
|
||||
explicitly declared/imported View facts.
|
||||
|
||||
`Exists` supports checked abstraction boundaries. A module can expose a value as
|
||||
"some representation `_repr` plus capabilities over `_repr`":
|
||||
|
||||
```text
|
||||
Exists _repr.
|
||||
Pair
|
||||
(Fn [String] _repr) -- constructor
|
||||
(Fn [_repr] String) -- renderer / eliminator
|
||||
```
|
||||
|
||||
This does not make raw Tree Calculus inspection impossible. Unchecked code can
|
||||
always inspect trees. It means checked clients cannot justify
|
||||
representation-specific operations through the View system unless the package
|
||||
exports an appropriate capability or eliminator.
|
||||
|
||||
This leads to an important distinction for future checked subsets:
|
||||
|
||||
```text
|
||||
controlled observation: Bool/List/Maybe/Result/etc. eliminators with Views
|
||||
raw observation: direct tree-shape inspection through triage-like power
|
||||
```
|
||||
|
||||
Useful application code can live mostly in the controlled fragment and receive
|
||||
explicit View validation over lambdas, application, let, and typed eliminators.
|
||||
Low-level library code may still use raw intensionality, but should expose
|
||||
disciplined Views and capabilities above it. Scott-encoded constructors and
|
||||
eliminators are a natural tricu-native representation for these APIs.
|
||||
|
||||
Tree Calculus terms do not carry intrinsic principal Views, and raw intensional
|
||||
code can invalidate parametric claims. View Contracts are an explicit evidence
|
||||
and contract layer over tricu programs; limited polymorphic Views are supported
|
||||
when they are declared or imported as facts with provenance.
|
||||
|
||||
The first stdlib annotation island starts with parametric functions that do not
|
||||
inspect representation:
|
||||
|
||||
```tri
|
||||
id x@_a =@_a x
|
||||
const x@_a y@_b =@_a x
|
||||
compose f@(Fn [_b] _c) g@(Fn [_a] _b) x@_a =@_c f (g x)
|
||||
```
|
||||
|
||||
Re-export-only modules preserve imported View metadata, so these contracts flow
|
||||
through `prelude` rather than only through direct `base` imports.
|
||||
|
||||
Functions built on raw `t`/`triage` should enter the checked world through
|
||||
trusted, controlled eliminator contracts rather than by treating arbitrary raw
|
||||
inspection as parametric.
|
||||
|
||||
|
||||
## 5. Guards
|
||||
|
||||
Guards are ordinary `tricu` values/functions grouped with the Views they refine.
|
||||
|
||||
@@ -123,7 +226,7 @@ Guards are injected by the checker. They are not discovered by the runtime as a
|
||||
separate metadata layer. The checking process transforms a view tree into an
|
||||
executable tree with the necessary guard applications inserted.
|
||||
|
||||
## 5. View Tree Artifact
|
||||
## 6. View Tree Artifact
|
||||
|
||||
The primary checker-facing artifact is a view executable term graph.
|
||||
|
||||
@@ -156,7 +259,83 @@ A node may contain opaque executable fields. Those fields are tree terms, but
|
||||
they are not recursively decoded as view-tree nodes or Views unless the node's
|
||||
semantics explicitly says so.
|
||||
|
||||
## 6. Checker Semantics
|
||||
View facts may also carry explicit per-fact trust provenance:
|
||||
|
||||
```text
|
||||
Checked -- derived by checked lowering / checker validation
|
||||
Trusted -- asserted by a trusted boundary, e.g. a primitive eliminator API
|
||||
Unchecked -- raw or assumed; no parametricity/abstraction guarantee
|
||||
```
|
||||
|
||||
In the portable view-tree envelope this provenance is represented as an optional
|
||||
field on `typedValue` / `typedRequire` facts. In module manifests the same
|
||||
provenance is carried beside the exported View Contract object reference so that
|
||||
imports and re-exports preserve it without relying on module-level convention.
|
||||
Absent provenance is interpreted conservatively as `Unchecked` at use sites.
|
||||
|
||||
For parametric checked definitions, the frontend now performs a conservative
|
||||
raw-intensionality dependency pass over local definitions. If a definition with
|
||||
scoped View variables depends directly or indirectly on raw `triage` / raw `t`
|
||||
construction, or on an imported `Unchecked` fact, lowering fails and asks the
|
||||
author to route observation through a trusted eliminator boundary. This is
|
||||
intentionally provenance/dependency based; it is not an attempt to decide
|
||||
whether arbitrary Tree Calculus reduction will ever reach rule 3.
|
||||
|
||||
View facts can be authored as ordinary value-level Tree Calculus metadata under
|
||||
one conventional top-level name:
|
||||
|
||||
```text
|
||||
viewFacts = [fact ...]
|
||||
fact = pair exportName (pair provenance view)
|
||||
```
|
||||
|
||||
where `exportName` is a string naming a value exported by the module,
|
||||
`provenance` is `0 = Checked`, `1 = Trusted`, or `2 = Unchecked`, and `view` is
|
||||
the same portable View record used by `view-tree` artifacts. The host evaluates
|
||||
this value and decodes the data schema; it does not infer trust from source
|
||||
syntax, AST shape, module name, or a Haskell-side catalog.
|
||||
|
||||
The initial trusted eliminator facts are authored this way in clearly separated
|
||||
stdlib `viewFacts` sections:
|
||||
|
||||
```text
|
||||
matchBool : forall r. r -> r -> Bool -> r
|
||||
matchMaybe : forall a r. r -> (a -> r) -> Maybe a -> r
|
||||
matchList : forall a r. r -> (a -> List a -> r) -> List a -> r
|
||||
```
|
||||
|
||||
The `base` module provides small `facts*` authoring helpers for this advanced
|
||||
metadata, e.g. `factsFact`, `factsChecked`, `factsTrusted`, `factsUnchecked`,
|
||||
`factsForall`, `factsFn`, `factsVar`, `factsBool`, `factsString`, `factsByte`,
|
||||
`factsUnit`, `factsMaybe`, and `factsList`. These helpers construct ordinary
|
||||
Tree data; authority comes from the exported `viewFacts` value and its explicit
|
||||
provenance tags. Loader validation rejects duplicate fact names and facts for
|
||||
names the module does not export.
|
||||
|
||||
Initial derived stdlib annotations using this trusted kernel include:
|
||||
|
||||
```text
|
||||
maybeMap : forall a b. (a -> b) -> Maybe a -> Maybe b
|
||||
maybeBind : forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
|
||||
maybeOr : forall a. a -> Maybe a -> a
|
||||
```
|
||||
|
||||
Recursive list combinators are currently published as explicit `Trusted`
|
||||
value-level facts rather than `Checked` source annotations, because their bodies
|
||||
pass through raw fixed-point machinery that the conservative parametric taint
|
||||
pass intentionally does not prove safe. This is the stabilized boundary: raw
|
||||
stdlib kernels establish conventions with explicit authority; ordinary checked
|
||||
clients consume those facts rather than re-proving the internals.
|
||||
|
||||
```text
|
||||
headMaybe / lastMaybe / nthMaybe
|
||||
append / map / filter / foldl / foldr
|
||||
length / reverse / snoc / count / all? / any? / intersect
|
||||
take / drop / splitAt / concatMap / find / partition / zipWith
|
||||
string/list-byte helpers such as strLength, startsWith?, lines, words
|
||||
```
|
||||
|
||||
## 7. Checker Semantics
|
||||
|
||||
The checker is an interpreter over the view tree.
|
||||
|
||||
@@ -184,7 +363,7 @@ or, in self-hosted terms:
|
||||
checkViewTree viewTree = ... -- ok checkedExec / err diagnostic
|
||||
```
|
||||
|
||||
## 7. Compatibility and Guard Injection
|
||||
## 8. Compatibility and Guard Injection
|
||||
|
||||
Structural compatibility is about Views. Guard injection is about producing the
|
||||
checked-execution tree.
|
||||
@@ -200,7 +379,7 @@ code that applies `userIdGuard` at the appropriate checked boundary.
|
||||
|
||||
The checker, not the runtime metadata system, owns this transformation.
|
||||
|
||||
## 8. Source Annotations
|
||||
## 9. Source Annotations
|
||||
|
||||
Source annotations are one frontend syntax for producing view-tree nodes.
|
||||
|
||||
@@ -222,7 +401,7 @@ that contains the relevant executable terms, views, and checking structure. The
|
||||
artifact must not depend on source names or on the frontend implementation that
|
||||
produced it.
|
||||
|
||||
## 9. Contract Expressions
|
||||
## 10. Contract Expressions
|
||||
|
||||
Contract-expression helpers remain useful as authoring/building tools, but they
|
||||
are not the fundamental artifact model.
|
||||
@@ -240,7 +419,7 @@ mapBoolStringUse = cFn <|
|
||||
These helpers should be understood as convenient ways to build typed/checkable
|
||||
structure, not as a permanent replacement for view-tree artifacts.
|
||||
|
||||
## 10. Artifact Direction
|
||||
## 11. Artifact Direction
|
||||
|
||||
The target direction is to make the view tree the canonical checked-program
|
||||
artifact.
|
||||
@@ -264,7 +443,7 @@ Do not store code over here and contracts over there.
|
||||
Store a view tree: executable code plus the structure needed to check and guard it.
|
||||
```
|
||||
|
||||
## 11. IO Interaction Trees
|
||||
## 12. IO Interaction Trees
|
||||
|
||||
`tricu` IO is represented as ordinary interaction-tree data:
|
||||
|
||||
@@ -324,7 +503,7 @@ may validate every continuation-produced action structurally, carry checked
|
||||
wrappers with higher-order function values, or define a portable checked-IO
|
||||
artifact instead of relying on Haskell/frontend source instrumentation.
|
||||
|
||||
## 12. Host Independence
|
||||
## 13. Host Independence
|
||||
|
||||
No part of the core View Tree design is specific to Haskell or to the current implementation.
|
||||
|
||||
|
||||
Reference in New Issue
Block a user