1 | ||||
|---|---|---|---|---|
2 | variable name | Universes | types in the universe | description |
3 | c, d, e | Core | D, F, FF, M, R, U, V | the core representation types |
4 | c, d, e | CoreN | Core or N | N delays representation (for DCs) |
5 | ss, ts, us, dcs | TSum | V, N t, :+ | just a sum, where the N arguments are the summands |
6 | ss, ts, us, dcs | All u, Exists u | certain TSums | all (resp., some) types in the TSum inhabit the universe u |
7 | dc | DCU t | t's constructor types | the constructors of DCU t are predictably named |
8 | t | DTU t | t's binding group | the constructors of DTU t are predictably named |
9 | dc | DCOf t | t where (DC dc, t ~ Range dc) | a different perspective on DCU t -- they should be isomorphic, but this universe has type constraints, whereas DCU t isn't expected to |
10 | dc | IsDC | dc where DC dc | (hasn't actually appeared in the library yet) |
11 | t | Uni ts | the types in the TSum ts | |
12 | dc | TagGistEQ m dc | dc's with the same Tag and Gst as dc | |
13 | t | EmjectIntoD el | t where DCs (App el (Range dc)) ::: Exists (TagGistEQ (ElabByT el) dc) | data constructors that can be elaborated according to the elaboration scheme el |
14 | fn | MFun m t | e.g. ToAt m n t, Pi u f | type/value-functions that affect the mediator: maps (App m t) to (App (MApp fn m) t) |
15 | fn | MMap c m | e.g. MFun.Map fn | MMap extends MFun; maps (RM m c) -> (RM (MApp fn m) c) |
16 | ||||
17 | Classes of Universe | example universes in the class | User-perspective | |
18 | Named | DCU t, DTU t | clear | |
19 | Structural | (:=: a), u :|| v, Uni ts | obfuscated | |
20 | Closed | DCU t, DTU t, (:=: a), u :|| v, Uni ts | membership is only affected by instances of other "closed classes" | |
21 | Open | TagGistEQ m dc, MFun m t | membership is affected by instance declarations | |
22 | First-order | DCU t, DTU t | ||
23 | Higher-order | u :|| v, u :&& v, Exists u, All u | ||
24 | Finite | DCU t, DTU t, (:=: a), Uni ts | a finite universe u is isomorphic to some Uni ts; namely Uni (Inhabitants u); see the Finite type class | |
25 | ||||
26 | Universe-quantified Data | quantification | use | |
27 | Sigma u (f :: * -> *) | universe-bounded existential | a type inhabiting u, and an f-value indexed-by that type | |
28 | Pi u (f :: * -> *) | universe-bounded universal | an f-value indexed by any type inhabiting u; a natural transformation u -> f | |
29 | Each ts (f :: * -> *) | = Pi (Uni ts) f | an f-value indexed by any type inhabiting Uni ts | |
30 | ||||
31 | Type Families | summary | description | |
32 | App m a | applies m as a type-level function | the consequent non-injectivity (as opposed to (m a)) is crucial to the Gist class, and hence Emject and Elab | |
33 | Pred u a | decidable inhabitation predicate; returns a type boolean | ||
34 | Find u c | finds a path to (N t) in c where t ::: u | related to Exists | |
35 | Range dc | the type dc constructs | ||
36 | DCs t | = Inhabitants (DCU t) | ||
37 | Siblings t | = Inhabitants (DTU t) | ||
38 | DTU t | a universe of t's binding group | ||
39 | Unwrap (f :: *->*) a | computes payload of (f a) | see Wrapper class; this lets us eliminate most newtype wrappers from the interface; it's built into Pi | |
40 | MApp fn m | applies fn as a function on mediators | isomorphic to App, just semantically difference; the result ought to also be a mediator | |
41 | Tag dc | the type-level serialization of the data constructor's name | crucial to Emject and Elab | |
42 | Rep a | the Core structure of a (NB no Ns) | library only uses instances for data constructors | |
43 | Inhabitants u | TSum of types inhabiting a finite u | ||
44 | Gst c m | folds m into RM m c | allows conversion between RM m c and RM n d if they're structurally equivalent; see Gist class | |
45 | ||||
46 | Data Families | |||
47 | DCU t a | a universe of t's constructors | ||
48 | RM m c | recursion-mediated Core | this is one of 2 prinicipal representations of data in the library | |
49 | ||||
50 | Type Classes | summary | notes | |
51 | t ::: u | inhabitation relation | ||
52 | Finite u | is finite | ||
53 | Wrapper f | Unwrap f a <-> f a | ||
54 | DT t | is-a datatype | ||
55 | DC dc | is-a constructor type | ||
56 | UniqueDC dc | is-a *-type's only constructor | e.g. a newtype or a partitioned GADT | |
57 | Reduce m ts | generic bottom-up reduction | can this just be a universe, like MFun/MFunRM? Perhaps MFold? | |
58 | Gist c | RM m c <-> Gist c m | probably refactor as a specialization of Wrapper | |
59 | Generic a | RM m (N t) <-> RM m (Rep t) | a slight twist on the ubiquitous class | |
60 | ||||
61 | Data representations | examples | description | |
62 | "(banded) datatype" | Nominal Datatype | standard Haskell datatypes | anything declared via data or newtype (or a data family instance, I suppose) |
63 | "disbanded datatype" | Disbanded m t | = AnRMN m (DCOf t) | |
64 | "an RMN Uni" | AnRMNUni m dcs | = AnRMN m (Uni dcs) where dcs ::: All IsDC | each dc need not have originated from the same type |
65 | "an RMN" | AnRMN m u | = Sigma u (RM m :. N) | |
66 | "(recursion-mediated) Core" | Recursion-mediated Core | RM m c where c ::: Core | all type names have been abandoned |
67 | "sigma, pi, each" | Universe-quantified | Sigma, Pi, Each | |
68 |