Last week was reading break but it was raining half the time and today, on our first day back, it's bright and sunny outside
This is injustice and I don't want to do work

Piano arithmetic

Anyway I'm gonna go hallucinate some match expressions

On the occasion that I do dream about code it's never about code I like
Last time it happened I hallucinated some Javascript for drawing SVG elements

The only downside to Microsoft Whiteboard is that I'll move a big chunk of drawing and it'll spend two minutes thinking about it

re: it's a long one about inductive definition universe levels

I installed Coq and tried it out and indeed the parameters can be anything, even types larger than the inductive type's universe itself. So that's that then, I'll fix my rules

it's a long one about inductive definition universe levels

I'm suddenly having trouble thinking about how my universe levels work... I think this is correct?
I've looked at some references and Coq's manual is the only one that says that the constructor's type's sort has to be the sort of the inductive type overall. So if I have a constructor like:

c: B -> C -> D -> X p a

And I have

B -> C -> D -> X p a: Type_i

Then that means that:

• A, B, C's types are all at most Type_i
• X's type is something like P -> A -> Type_i

But the thing is that this doesn't quite tell me what the sorts of P and A are, so I'm not sure if X's type should have sort Type_{i+1}
But in the constructor's type, the index a comes from some combination of the arguments B, C, D, and those have sort Type_i, so surely A must also have sort Type_i... right?
But not the parameters... Those could be anything...

What if I add a Prop hierarchy without actually adding any rules for proof irrelevance lol
It'll just be hanging out there nbd
You can make it impredicative or proof irrelevant if you like

I made it slightly better by using \Gamma and \Delta in places where there were ... but it's still ungood

I didn't want to use w but I ran out of letters

I added parameters back in. As expected, it is uglier

Back to envs, the Type Checking with Universes paper uses Θ and Ψ, but the thing I want is decidedly not an env, so maybe I should avoid those
That leaves Ξ Φ Ω

I find that there's a camp of people who like to use M N for terms and A B for types, and then another camp who like e for terms and \tau for types, and yet another who like t for terms ans T for types, and then the rest just mix and match from those

Today's endeavour: picking yet another capital Greek letter to represent a sequence of constructor definitions (not a telescope, since I don't think latter constructors may depend on earlier ones), because I've already used up \Gamma, \Delta, and \Sigma
I'm thinking one of these: Θ Ξ Φ Ψ Ω

"number theory is like IHOP -- you never actually decide to go there, you just end up there"

i feel like i need to make one of those "we have been played for absolute fools" memes about category theory

let. ramble

I think it's because the type of the fixpoint cannot use the fixpoint itself (which would be really weird), only the body, and let expressions need the assignment available to correctly check the type of the body
I have a feeling that a fixpoint whose type refers to the fixpoint itself is one of those Very Dependent Functions that some NuPRL paper references

let. ramble

Why don't the premises of fixpoint typing need to have the definition of the fixpoint in the environment during typing?

let. ramble

I like let definitions very much but the thing that has bothered me is that it a) it doesn't fit into the grand scheme of form/intro/elim/comp rules, and b) it affects the shape of the environment
I think it's a very profound thing, that what goes into the environment must differ due to just a new term, but the logic or math people probably have figured out what it means in the proof theory sense
In any case, it's rather underutilized, given that only the let rule uses them

Anyway it's 1:30 am and I've decided to add parameters back in because a) I know how to not have ugly substitutions everywhere now and b) the fewer conventions of yore I go against the better... for now

Show older

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.