hazelgrove / hazelgrove Goto Github PK

These were in the reviews:

hazelgrove/obt2017#1

At the talk:

1. conor mcbride's thesis in detail
2. labeled lambda calculus

@cyrus- other stuff that you took notes on while i was in dissociative fugue talk state?

i have no idea why i did at least one thing in the minimizer; the case for subsuming concase1 pattern matches on the argument derivations and nothing else does. so it's actually banning something at a much finer granularity, only in one situation, and determinism goes through.

so why don't the other ones do that too?

what is the minimal minimizer? and how do we prove that we have it? i thought we did, but now i bet we don't.

this may be related to why the proof of trying to show that the derivation produced by the minimizer is the same as the input if it's minimal didn't go through. or is that a property that's going to be true once we work out the proof technique for any notion of minimization?

one for ones that the system inserts and removes automatically, one for ones that the programmer doesn't want messed with because they're exploring something.

ought to be able to prove something about autofinishing / preservation of finish normal form. (which I always hear as "Finnish normal form".)

hazelgrove/agda-popl17#5
hazelgrove/agda-popl17#4

hazelgrove/agda-popl17#33

add a theorem about "we expand to the most informative type". that means we need to say that t' is more informative than (at least as informative as) t' in the analytic expansion, and therefore to define a lattice on types in this way. it's probably in the gradualizer work.

What is the worst-case behavior for processing an arbitrary sequence of user actions by (naively) doing type-checking from-scratch after each user action in the sequence?
(That is, is it possible that the naive approach would require re-processing the entire term after each action?)

Is there a role for doing incremental bidirectional type checking? (That is, is there a role for caching and reusing the work of type-checking?)

hazelgrove/agda-popl17#17

http://hilton.org.uk/presentations/beautiful-code
Here are some cool ideas

Hazelnut currently consists of a theory that explains (bidirectional) type-checking of terms that contain holes; further, the holes can be filled with partially-constructed terms that do not match the type required in an outer term that contains the hole. In essence, the use of holes permits the user to systematically construct terms that contain missing pieces, or mis-matched sub-terms.

Given this, how do we normalize λ-terms that contain such (empty or filled) holes in their terms?

What should the meta theory of normalization be?
(Do we have a property like subject reduction, and/or progress + preservation?)

http://unisonweb.org/
someone pointed me to this on twitter today. I was not familiar with it before.

Any ideas for logos or iconography, for either Hazelnut or Hazelgrove?

Some image ideas:

• Hazel tree leaves and nuts
• Photo of a hazel tree grove

Related: This section from wikipedia an interesting read, it claims: "The Celts believed hazelnuts gave one wisdom and inspiration."

hazelgrove/agda-popl17#18

we don't really know how ~ works with <=. @cyrus-'s intuition is something like ∀{Γ e t t'} → tcomplete t → Γ ⊢ e <= t → t ~ t' → Γ ⊢ e <= t' but i can't prove it as stated. it's not relevant to anything in the POPL paper, it's just a structure that we have some intuition about that we can't pin down.

hazelgrove/agda-popl17#2

hazelgrove/agda-popl17#21

it's pretty hard to prove something simple even just like this without getting stuck in a loop; there's got to be some metatheory here that lets us work with traces.

  ex5 : ∀{Γ e' e◆ t'} →
          (Σ[ L ∈ List action ]
             ((runsynth Γ (((N 3) ·:₂ ▹ <||> ◃) ∘₁ (N 4)) <||> L e' t')
               × erase-e e' e◆
               × ecomplete e◆))
          → ⊥

hazelgrove/agda-popl17#25

possibly relevant to doing things in Coq in the future as well.