Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Usage polymorphism, dependent usage brainstorming #87

Open
cwgoes opened this issue Sep 5, 2019 · 5 comments
Open

Usage polymorphism, dependent usage brainstorming #87

cwgoes opened this issue Sep 5, 2019 · 5 comments

Comments

@cwgoes
Copy link
Collaborator

@cwgoes cwgoes commented Sep 5, 2019

An example, with Church-encoded naturals:

one :: 1 (1 (a -> a) -> 1 a -> a)

two :: 1 (2 (a -> a) -> 1 a -> a)

three :: 1 (3 (a -> a) -> 1 a -> a)

where, ideally, we have

succ :: 1 (1 (n (a -> a) -> 1 a -> a) -> ((n + 1) (a -> a) -> 1 a -> a)

I can think of a few options here.

1 - Typeclass-style usage polymorphism in the frontend language

Frontend language level usage polymorphism, where succ must be instantiated for an n known at compile time at each call site (like a typeclass), and must be instantiated with w if n is unknown at the call site. This is easy, but probably not that useful, since often we won't know n for the argument at compile time.

2 - Usage polymorphism in the type theory

Add a forall u . T, where u ranges over the semiring, to the core type theory, and can then appear as a variable for any usage in T. This then will require n-variable polynomial constraint satisfiability checks during typechecking, but should have zero runtime cost (I think). It may impact the kinds of memory management we can automate, not sure yet, but we should still have more information than without quantization at all (or, equivalently, with w).

3 - Dependent usaging in the type theory

(possibly - probably - crazy)

Add a ↑u term to lift a term to a usage, such that usages in T in a dependent function of type (𝜋 𝑥∶ 𝑆) → 𝑇 can depend on x (we must then choose some canonical bijective mapping between semiring elements and terms), and some sort of beta-equivalence proofs of usage correctness will be required of programmers using this kind of lifting (in order for the term to typecheck). (possibly also add a usage-to-term ↓u, not sure)

@andy-morris

This comment has been minimized.

Copy link
Contributor

@andy-morris andy-morris commented Sep 17, 2019

Inspired GHC-Haskell's TYPE being parameterised by a RuntimeRep, I wonder if maybe for option 3 we may be able to have usages be defined inductively inside the language as, e.g.,

data FiniteUsage = Zero | Suc FiniteUsage
data Usage = Finite FiniteUsage | Omega
-- plus shorthand for numeric literals, "ω", or what have you

and a type rule along the lines of

  0Γ ⊢ S:⁰ ★ᵢ
  0Γ, x:⁰ S ⊢ T:⁰ ★ᵢ
  0Γ ⊢ u:⁰ Usage
-----------------------------
  0Γ ⊢ Π(x:ᵘ S). T:⁰ ★ᵢ

We could then allow whatever computation over usages that people could possibly want.

One downside is that proving anything about this system might be, um, challenging.

@cwgoes

This comment has been minimized.

Copy link
Collaborator Author

@cwgoes cwgoes commented Sep 17, 2019

We may be able to have usages be defined inductively inside the language

Would there be custom introduction rules for u :⁰ Usage then (referencing these constructors)?

Lambda-encoded ADTs is clearly not what we want in this case.

It would be interesting (debatable: whether it would be preferable) if the user could define a "special datatype" to be Usage, for which appropriate introduction rules would be created (maybe proofs of semiring-ness could be required). I don't know if there are really that many interesting options, though - the natural numbers plus omega provides both precision and flexibility - are there other semirings that would be advantageous?

Less radical is to do this in the type theory but not allow the user to change it (just allow usages to be constructed as terms and then "lifted" via this type rule) - is that what you mean?

We could then allow whatever computation over usages that people could possibly want.

Hmm, how would dependent usages work - would there be a conversion rule for usages (based on beta equality) that could then be used e.g. to type multi-argument functions where the usage of some arguments depended on the values of previous ones?

@andy-morris

This comment has been minimized.

Copy link
Contributor

@andy-morris andy-morris commented Sep 27, 2019

To be clear, I wasn't proposing having an arbitrary user-defined datatype for usages! That could be interesting, but for now I was just thinking of making the ℕ∪{ω} structure accessible inside the language.

There may be something obvious I'm missing, but it seems like we could use the same equality for usages as for any other terms? As far as I can tell there doesn't seem to be any significant difference between

replace-π = subst (λ π' → ((π x: A) → Z)) eq-π f
replace-A = subst (λ A' → ((π x: A) → Z)) eq-A f

-- where
-- eq-π : π ≡ ρ for some π, ρ : Usage
-- eq-A : A ≡ B for some A, B : Type
-- subst : {0 A : Type} (0 P : A → Type) {0 x y : A} → 1 x ≡ y → 1 P x → P y
--   i.e. induction for _≡_

And outside of explicit uses of subst we'd just use αβη-equality?

@cwgoes

This comment has been minimized.

Copy link
Collaborator Author

@cwgoes cwgoes commented Sep 28, 2019

As in, we would define a conversion rule for usages based on a usage type and αβη-equality on the type?

@cwgoes

This comment has been minimized.

Copy link
Collaborator Author

@cwgoes cwgoes commented Nov 20, 2019

Notes on first-class usages:

first-class-usages

(also see this PR - #99)

Notes on post-first-class-usages (very tentative, just a list of ideas):

post-first-class-usages

Incidentally, these blog posts on OTT might be useful - 1, 2.

@cwgoes cwgoes added the juvix-1.0 label Dec 14, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked pull requests

Successfully merging a pull request may close this issue.

None yet
2 participants
You can’t perform that action at this time.