Practical Types

Stream: Type theory

[Steven Obua]

Hi, I've come up with a new logic called "Practical Types". I would say it is basically first-order logic with types as axiomatic basis. Free variables can depend on parameters, though, I need that so that there is a powerful definition mechanism. I've written up details about it at https://doi.org/10.47757/practical.types.1 and would love to chat about it, and related approaches!

[Mario Carneiro]

(FYI: This was forked from a discussion at FMM.) My position is that it is both possible and advantageous to have a proof assistant use a type theory that is implemented on an untyped foundational system such as FOL / ZFC, and use the underlying logical rules as inspiration for the things that the type theory is allowed to do. For example, extensional types are a natural addition, as well as dependent types. I'm not really sold on universes, I think that this is an artificial consequence of type theoretic foundations.

[Mario Carneiro]

Regarding the practal axioms, it would be useful to have a model of those axioms implemented in a formal system, because there are rather a lot of them and some of them are quite strange on first look; besides putting any worries about consistency to rest, it also provides readers with a clear mental model for the meaning of the assertions

[Mario Carneiro]

I mentioned MM0 briefly before. I imagine it developing a type system such as I've described eventually, but right now it's mostly only at the "untyped foundation" level; you have to manually manipulate (what you would think of as) typing predicates.

[Steven Obua]

I've looked at MM0 last year. Do you have a strategy for building up theory developments without introducing new axioms all the time, i.e. does MM0 follow the LCF approach?

[Mario Carneiro]

That depends on what you mean by LCF approach. The usual interpretation of this in HOL based systems seems to involve an abstract data type and ambient programming language, and to that end it does not follow LCF; if you mean does it have a small kernel then yes; and if you mean can you get a lot done once you have stopped adding axioms then yes

[Mario Carneiro]

the principle mechanisms for the latter are the ability to make new definitions and prove theorems / inference rules as lemmas

[Steven Obua]

As to practal axioms, yes, it would be great to have a model, for example in ZFC. I suspect you will need additional axioms like discussed last year.

I haven't combed the axioms yet for minimality (yet), I've just added everything that I thought makes sense and might still be consistent :-) Further cleanup should be possible. I think the axioms are all pretty straightforward, is there any axiom you are worried about in particular? I think there is no way around universes, as you will want every object to have a type.

[Mario Carneiro]

In fact, most of the axioms bear a striking resemblance to metamath's "type system" in the set.mm math library based on ZFC

[Steven Obua]

What I mean by LCF approach is the following: There is a build up phase where you introduce the axioms. Then EVERYTHING else is introduced by definition and cannot cause inconsistency (assuming the build up phase didn't already).

[Mario Carneiro]

for example stuff like nil x = nil holds (written ( (/) ` x ) = (/) where the empty set plays the role of nil)

[Steven Obua]

I would expect them to, because types in practal are basically sets, but with data abstraction.

[Mario Carneiro]

sure, doesn't every system do that?

[Steven Obua]

I wasn't sure about MM0 in that respect!

[Mario Carneiro]

well okay that's not true for metamath

[Mario Carneiro]

it is true for MM0 though

[Mario Carneiro]

that's one of the major departures - it has a built in definition checking mechanism

[Mario Carneiro]

in metamath there is an external definition checker which is good but not great since it is still important for soundness if you don't want to trust thousands of axioms

[Mario Carneiro]

Steven Obua said:

I would expect them to, because types in practal are basically sets, but with data abstraction.

Could you explain what you mean by data abstraction?

[Steven Obua]

In Practal you have ∅ x = nil though. The empty set and nil are kind of dual in practal.

[Steven Obua]

I mean that the space of functions in Practal really is just a space of functions, for example. A function is not a set, also, or has any other structure beyond being a function.

[Mario Carneiro]

that would still be fine as long as you choose not to talk about the set structure

[Mario Carneiro]

metamath does sometimes talk about the set structure of functions though, for example intersection of functions is a thing

[Steven Obua]

Well, it violates data abstraction for them to be sets. It's not a good thing.

[Mario Carneiro]

sure, but I'm talking about the underlying foundation, not the "front end"

[Steven Obua]

yes, me too

[Steven Obua]

Let's say you define addition. Once you have defined addition for sets, that's it. You cannot change it for functions.

[Steven Obua]

By types being independent from each other, each can have their own addition operation, and still everything can stay consistent.

[Mario Carneiro]

In lean, those would be two different addition functions, and you are using "typeclass inference" to distinguish them based on their ambient types

[Steven Obua]

Basically type extensionality gives you all the good properities of sets, and none of the bad

[Mario Carneiro]

I would find it somewhat sketchy to have those be the "same" addition

[Mario Carneiro]

in metamath they are literally different functions, you will write A +s B and f +f g or something

[Steven Obua]

Well, what I am saying is if your underlying foundation is set theory, you have no other choice than being sketchy

[Mario Carneiro]

you can just have additional arguments to the function, or different functions

[Steven Obua]

Well, as Lean proves, and Isabelle, and Coq, you can do all sorts of things

[Mario Carneiro]

lean does it by having an additional argument, inferring it, and suppressing it in printing

[Steven Obua]

But how simple is it? I don't want additional arguments, because they make things more complicated.

[Steven Obua]

In practal, a function is a function. It doesn't need additional type arguments etc.

[Mario Carneiro]

metamath doesn't like the complication and magic of implicit args so it uses different functions

[Mario Carneiro]

But using the same function says something significant about the domain that you don't always want and is sometimes impossible to satisfy

[Steven Obua]

But each of these different functions is still defined on everything, because everything is sets

[Mario Carneiro]

Not necessarily, +f might be defined on pairs of functions with the same/compatible domains

[Mario Carneiro]

and if you use it on a non-function you just get (/) aka nil

[Steven Obua]

let me put it the other way around: what is your argument AGAINST types like in Practal

[Steven Obua]

Are you against data abstraction?

[Mario Carneiro]

At the low level, yes

[Steven Obua]

why?

[Mario Carneiro]

more ontological entities means a more complex theory to reason about and prove the soundness of

[Mario Carneiro]

The low level theory should be the bare minimum needed to build mathematics

[Mario Carneiro]

and it should ideally be a system that logicians know a lot about

[Mario Carneiro]

or reducible to such

[Steven Obua]

Well, in Practal there are propositions, functions, natural numbers, and types.

[Steven Obua]

That's it. I think that is as simple as it should be.

[Steven Obua]

It makes no sense to mix up any of these with each other.

[Mario Carneiro]

But I assume you agree that you could do the same things even with fewer categories

[Steven Obua]

no, I don't , and I would not want to.

[Mario Carneiro]

the thing data abstraction (or typing in general) gives you is the ability to say no to things

[Mario Carneiro]

but you don't need the foundational theory to do that

[Mario Carneiro]

the front end can do that just fine

[Steven Obua]

Yes, if you want your foundational theory, and your practical theory to be the same, you need to

[Steven Obua]

A front end just makes everything more complicated

[Steven Obua]

I thought you want simple?

[Mario Carneiro]

I don't think that should be a goal at all

[Steven Obua]

It doesn't have to be like that

[Mario Carneiro]

The front end needs to support the practice of writing mathematics, which is entirely separate from the goal of verifying mathematics

[Steven Obua]

If you can get significant advantage by separating the two, by all means do it

[Mario Carneiro]

For example, lean has tactics in order to support the front end experience

[Steven Obua]

No, you write mathematics so that it can be verified by other people

[Steven Obua]

A good front end is great.

[Mario Carneiro]

If you try to make the foundation the same as the front end, you will just feel a constant push to make the foundation more complicated

[Mario Carneiro]

that's how DTT got the way it is

[Mario Carneiro]

and it will never be good enough

[Steven Obua]

I understand your concerns, and I agree, that is true for static type systems.

[Mario Carneiro]

because users' desires for convenient mathematical data entry are infinite

[Mario Carneiro]

I certainly don't want to have a neural network in the kernel

[Steven Obua]

Haha, me neither.

[Mario Carneiro]

but I also don't want to have to tell users that they need to be spartan to use the system

[Steven Obua]

I want the foundation to be as simple as possible, while allowing me to do everything important without tricks.

[Steven Obua]

As I said, there is no need to be simpler than functions, propositions, types and natural numbers.

[Steven Obua]

It would be great to build a model in something simpler.

[Steven Obua]

But that's it.

[Mario Carneiro]

Lean and Coq and Isabelle have all done a good job of providing a generous arena for doing mathematics. Isabelle is the only one of those that has mostly managed to keep that complexity out of the kernel

[Steven Obua]

But they are all not good enough in what you can do in them.

[Steven Obua]

Practal will have a simpler kernel, and a more powerful one.

[Steven Obua]

When you say frontend, I think of the parsing mechanism I implemented so far.

[Mario Carneiro]

There aren't too many places where I would say that lean is (foundationally) too weak for what I want to do; the main area is around the straightjacket of intensional type theory

[Steven Obua]

Sure, that's complexity that has no business being in the kernel.

[Steven Obua]

For example lean has no subtyping, and no undefinedness. That's pretty bad.

[Mario Carneiro]

It has both, through types

[Steven Obua]

It has none, because of types.

[Mario Carneiro]

Subtyping is done via implicit "coercion" injections, and undefinedness is done through the option type

[Steven Obua]

All it has are workarounds.

[Mario Carneiro]

Perhaps, but you have to show evidence that the workaround is inadequate for solving real problems

[Steven Obua]

And these things cause a lot of pain. Like you have to change your whole formalisation in order to accomodate for that.

[Steven Obua]

No, I don't have to. You can do everything with workarounds. It is just not as good as it could be.

[Mario Carneiro]

Honestly that is true in any system. You always have to formalize taking into account the constraints of the system, and no system is unconstrained

[Steven Obua]

Practal is about as unconstrained as you can possibly get it.

[Mario Carneiro]

Maybe you have subtyping, but do you have the right subtyping? Maybe it doesn't actually match mathematical practice

[Mario Carneiro]

what do you do then?

[Steven Obua]

If you have type extensionality, then subtying follows automatically from that. There is only one kind of subtyping then.

[Mario Carneiro]

You give an example of this on that practal page: you would like A -> B <= C -> D iff C <= A and B <= D but it doesn't work for technical reasons

[Mario Carneiro]

but that won't stop people from not liking that it fails

[Mario Carneiro]

in lean this would work just as well as any other subtyping relation

[Steven Obua]

Well, some things are just how they are. Subtyping does certain things, and not others.

[Mario Carneiro]

because subtyping is not limited to embeddings in some global sense

[Steven Obua]

I would say coercions are a frontend as you describe it.

[Mario Carneiro]

they certainly are

[Mario Carneiro]

or rather, the syntax mechanisms to insert them and elide them when possible is a front end feature

[Steven Obua]

And there is no problem with that. You can define functions between different types in Practal. As a syntactic feature, you can have coercions in Practal.

[Steven Obua]

But you cannot have subtypes in Lean.

[Mario Carneiro]

if they are automatically inserted, never visible and never interact with any theorems you apply, then to the user they may as well not be there

[Mario Carneiro]

how does that differ from having "true subtypes"

[Steven Obua]

Because it is not like that. I have no experience with coercions in Lean, but I am sure they are never completely invisible.

[Steven Obua]

Subtypes are. By design.

[Mario Carneiro]

oh but they aren't

[Mario Carneiro]

what you forget is that subtyping has a consequence around decidability of typing

[Mario Carneiro]

when you can't say what type a thing has, type inference takes a hit and applying lemmas gets more painful

[Mario Carneiro]

there is no free lunch

[Steven Obua]

But that is frontend stuff. Type inference is frontend.

[Mario Carneiro]

now it's a tradeoff, and it might be worth it depending on factors, but you have to weigh that against the gains that literal subtyping give you over "simulated subtyping"

[Steven Obua]

Yes, and I weighed that. simulated subtyping lost.

[Mario Carneiro]

You say you don't have much experience with coercions so I'm not sure you have actually considered the options thoroughly

[Mario Carneiro]

you are right that coercions aren't always invisible, but until you know the pros and cons I'm not sure you can judge the relative benefit of literal subtyping

[Mario Carneiro]

I am a fan of the literal subtyping that you have in metamath for things like 1 \in Z -> 1 \in R, but it's also very nice that n : int -> n : zmod 37 works in lean, and I know there is no way that's going to happen in metamath because literal subtyping is tied to the concrete representation of objects

[Steven Obua]

I don't think I can convince you otherwise, and I don't want to convince you based on what
I am thinking about subtyping.

[Mario Carneiro]

I'm just saying there are advantages on both sides, and don't be too dogmatic about it

[Mario Carneiro]

coercions aren't completely intolerable

[Steven Obua]

I am not. If coercions are possible in Practal, I want them. I just know that type extensionality I want for sure, and subtyping follows from that.

[Mario Carneiro]

but you have to experience them for yourself to see just how intolerable they are

[Steven Obua]

I have used coercions in Isabelle.

[Steven Obua]

And you don't need much experience to say what their problem is.

[Steven Obua]

There is something in your theorems, that is there, but you cannot see. But in some cases, it is important.

[Steven Obua]

Obviously there are always going to be problems with such an approach.

[Mario Carneiro]

type extensionality is another interesting thing. In lean you don't have type equality except in trivial cases, but in a system that takes data abstraction seriously like practal it's not clear to me that you can do much better

[Mario Carneiro]

Note that in lean, coercion is displayed as an up arrow operator, because invisible coercion is confusing

[Steven Obua]

But it can. Practal is evidence (except if it turns out to be inconsistent, of course).

[Mario Carneiro]

like you say, it's bad when something you can't see changes how a tactic works

[Mario Carneiro]

what kind of nontrivial type equalities are you getting?

[Steven Obua]

Yeah, so in that sense it could also work in Practal. You insert a symbol, and it means "coerce if undefined"

[Mario Carneiro]

Does practal have type inference?

[Steven Obua]

What "non-trivial" type equalities are you looking for?

[Steven Obua]

No, no type inference. Everything has to go through theorems.

[Mario Carneiro]

what's the point of the type theory then?

[Mario Carneiro]

that's not meant as judgment, I literally want to know why you want types without type inference

[Steven Obua]

Because types represent concepts. You want those concepts. It's that Lean and Coq etc. confuse them with types for programming.

[Steven Obua]

I want matrices. I want functions. I want functions of matrices. etc.

[Steven Obua]

And I like that a proposition is not a function. Because it is a different concept.

[Steven Obua]

Because, when I am thinking about functions, I don't want to have to think about propositions, too.

[Steven Obua]

There is no need for type checking in a theorem prover. I understand that it was convenient for a long time, given limited hardware etc.

[Mario Carneiro]

That's odd, I would say it the other way around

[Steven Obua]

Like how?

[Mario Carneiro]

It is more convenient now than ever and stronger computers help us do it more

[Mario Carneiro]

I have heard it said that type checking is the closest thing most programmers get to theorem proving, and type inference is automated theorem proving

[Mario Carneiro]

who would say no to that?

[Steven Obua]

Hahaha, that is not wrong.

[Mario Carneiro]

Knowing that there is a huge class of problems that can just be automated away, I would be a fool to pass it up

[Steven Obua]

But programming is not theorem proving.

[Steven Obua]

I said that before, I know.

[Steven Obua]

If types are there because they model my concepts, great.

[Mario Carneiro]

it's the baby version, although if you look at haskell and rust you will see some stuff that is nigh-indistinguishable from the work that goes on in actual mathematical theorem proving

[Steven Obua]

If they get in the way of me modelling my concepts like I want to, that's not acceptable.

[Steven Obua]

I think there is a certain kind of reasoning and thinking that programmers like to do, and Coq etc. are a good fit for that.

[Mario Carneiro]

There is a great MO post by andrej bauer about this that I need to dig up

[Steven Obua]

I would say programmers are more "syntax" based.

[Steven Obua]

I am more "semantics" based.

[Mario Carneiro]

https://mathoverflow.net/a/376973/34444

[Steven Obua]

"The field of scalars is not specified"

[Steven Obua]

Exactly that. If I have a vector space U, I don't need to specify the field of scalars. Because it is already part of it.

[Steven Obua]

I would hope that in Practal, you don't need either.

[Mario Carneiro]

You need the two vector spaces to have the same field though, I doubt you can get that for free with practal style

[Steven Obua]

But as he says, you can only find out the suitability for sure by doing it.

[Steven Obua]

Yes, but if you say stuff like you have a linear map from U to V, then you have it for free.

[Mario Carneiro]

because it is empty or because it is nil?

[Mario Carneiro]

otherwise

[Steven Obua]

Because it is part of the definition of what a linear map is.

[Mario Carneiro]

Getting the type of x and y in that example requires type inference, I think

[Mario Carneiro]

if you just say \forall x y, ... (do you have unbounded quantifiers?) then the equality is probably not true

[Steven Obua]

The type is built into the objects, no need for inference.

[Mario Carneiro]

not sure what you mean

[Mario Carneiro]

we are introducing two variables x and y and not saying the type

[Mario Carneiro]

that corresponds to a quantifier like \forall x, ...

[Steven Obua]

𝑓(2⋅𝑥+𝑦) =↓ 2⋅𝑓(𝑥)+𝑓(𝑦) will be true in Practal

[Mario Carneiro]

for what x and y

[Mario Carneiro]

Do they have to be in the type U?

[Steven Obua]

Let me check, I am not sure.

[Steven Obua]

2 * x + y needs to be in U, otherwise f(2 * x + y) would be nil

[Steven Obua]

likewise x needs to be in U, otherwise f(x) = nil, same for f(y)

[Steven Obua]

Because f: U -> V

[Steven Obua]

But what about the 2? and the "*" and the "+"

[Mario Carneiro]

so if I write \forall x y, 𝑓(2⋅𝑥+𝑦) =↓ 2⋅𝑓(𝑥)+𝑓(𝑦) then that's false

[Steven Obua]

oh sorry, the other way around anyway, you have to write =↑

[Steven Obua]

which means, if either of them is defined, then they are equal

[Mario Carneiro]

While I'm sure you can make some such variant work, that only works out some of the time

[Steven Obua]

But in this situation, you would probably want to write ∀ x y : U in the first place.

[Mario Carneiro]

I know because metamath does that kind of thing all the time

[Steven Obua]

The question is, how are general operators like "+", *" and "2" handled.

[Mario Carneiro]

for example if we were proving not-equals then the =↑ would cause problems

[Steven Obua]

That's overloading / type class stuff, and you would want some of that in Practal.

[Mario Carneiro]

I thought you wanted + to just mean different things on different sets

[Mario Carneiro]

like there is only one + and it somehow plays the role of all additions

[Steven Obua]

No, that was just an example that I don't want a definition on some set to automatically mean something on other sets.

[Steven Obua]

I imagine there to be overloading, and types can be used for that. That is one reason why they are superior to sets.

[Steven Obua]

So when I defined addition on natural numbers, I don't want to have to wonder what it means on other sets that are not natural numbers.

[Mario Carneiro]

But I hope you agree that overloading is not a feature of the foundation

[Mario Carneiro]

isabelle has overloading in the foundation and it's a nightmare

[Steven Obua]

It needs to be made possible for by the foundation, I think, but not a feature, no

[Steven Obua]

I know, I had my fair share of thinking about that ;-)

[Steven Obua]

I think you need conditional definitions in the kernel, to make it work though.

[Mario Carneiro]

What provision does the foundation need?

[Steven Obua]

and if you add another case, you prove the consistency of that case

[Mario Carneiro]

Not sure what you mean by conditional definitions, but I think that's the isabelle nightmare I mentioned

[Steven Obua]

No, Isabelle's problem is that it needs to statically determine if it is save or not.

[Steven Obua]

safe

[Steven Obua]

In principal it is simple. If you add a definition P ==> A = B, make sure that for all other other previous definitions P' ==> A = B', for those cases where both P and P' are true, B and B' coincide.

[Mario Carneiro]

Introducing a definition piecemeal sounds very sketchy to me

[Mario Carneiro]

how are you going to manage that context of previous definitions?

[Steven Obua]

And that is just a proof obligation for the definition mechanism.

[Steven Obua]

Well, there are only finitely many.

[Steven Obua]

It is what computers are there for.

[Steven Obua]

It is somewhat sketchy. But it is what you do in practice, because in practice you build your theories piecemeal.

[Mario Carneiro]

it means that I can't build a model incrementally by reading clauses, any potential model could be falsified later

[Mario Carneiro]

with plain definitions each entity is defined in terms of previous definitions

[Mario Carneiro]

Also you would get some asymmetry/order dependence when introducing clauses

[Steven Obua]

I have not thought through it properly. That's why I left it out of what I have written up so far.

[Steven Obua]

Maybe, because of types, you can do it entirely outside of the kernel, and you need no conditional definitions. And that would be actually great.

[Steven Obua]

But I think new types will possibly destroy models anyway?

[Mario Carneiro]

why would they?

[Steven Obua]

Because you create a new type, and now something exists that didn't before. Could that be a problem?

[Mario Carneiro]

You just have all types existing at the outset, and you are just using a grammar to select those types that exist already

[Mario Carneiro]

like in ZFC, the syntax {x \in A| P(x)} doesn't create a new type, it names an existing type

[Steven Obua]

Very platonic. Sounds reasonable to me, but I wouldn't do the model building in the first place. :-)

[Steven Obua]

In Practal, there are two different options here

[Mario Carneiro]

You don't need to do the model building, but it's useful to have that property for proof translation purposes

[Steven Obua]

You can write { x : A | P(x) }, which is just a subtype of A

[Steven Obua]

and you can write typedef B = { x : A | P(x) }, and now B and A are disjoint

[Steven Obua]

But I guess B could have existed before anyway

[Steven Obua]

Yes, for the foundations it should be clear how to build the model. But then the user can forget about it, because Practal ensures, whatever they do, it's fine, there still will be a model.

[Steven Obua]

And there are different options for typedef so that you can do quotient types, and glue other existing types into the new type.

[Mario Carneiro]

One way to model that (in ZFC, say) is that you have a designated space for typedefs, for example you have pairs (i, x) where i is a natural number and x is any set, forming omega many copies of V, and the nth typedef selects a subset of V_n

[Steven Obua]

Yes, this is similar to what we talked about last year, isn't it

[Mario Carneiro]

Even if you could make partial definitions work, I think it would not be good enough for the uses that people want overloading for, though. For example you might want + to mean one thing on A and a different thing on B (using context to distinguish them), despite the fact that A and B are not disjoint

[Mario Carneiro]

I know there are examples of such in lean

[Mario Carneiro]

in fact the whole "newtype" pattern is specifically so that you can make the same notations on the same elements mean something different

[Steven Obua]

Yes, I think I agree with you.

[Steven Obua]

I just mixed things up.

[Steven Obua]

But I have to think about it properly first because I can agree definitely.

[Steven Obua]

But yeah. This is what types are great for, and sets are bad at.

[Mario Carneiro]

The way I see it, the type checker maintains, for each expression, a typing judgment that is "the type" of the value, and uses that to answer questions like what type does this value have, how to I resolve this notation, etc

[Steven Obua]

But let's say I define addition on natural numbers.

[Steven Obua]

Later on, I introduce real numbers that have natural numbers glued into them.

[Steven Obua]

Now I need to extend the definition of addition.

[Mario Carneiro]

but then there is some additional mechanism for saying "note now that x also has this other type" and then you can do literal subtyping

[Mario Carneiro]

I think Mizar has a reconsider directive that does approximately this

[Steven Obua]

I don't know how something like that would work in Practal's logic.

[Mario Carneiro]

Which part? It looks pretty natural for soft typed systems

[Steven Obua]

You define plus : Nat -> Nat -> Nat

[Steven Obua]

What about plus : Real -> Real -> Real?

[Mario Carneiro]

Well in my setup you would have a different function plus_real : Real -> Real -> Real, but then set notation up so that you can use + for both plus_nat and plus_real

[Steven Obua]

If Real and Nat would be different types, that would be the way to go.

[Mario Carneiro]

and the system infers which one you want based on "the type" of the arguments

[Mario Carneiro]

which is why the type checker needs to be able to answer questions about the types of things

[Steven Obua]

But there is no type inference in Practal.

[Mario Carneiro]

the method I'm describing gives you type inference too

[Steven Obua]

No, there can be no type inference, otherwise it doesn't work

[Mario Carneiro]

Why is that?

[Steven Obua]

Equality can not be based on type inference, equality just "is"

[Mario Carneiro]

I didn't say anything about equality

[Steven Obua]

What does x + y mean then?

[Mario Carneiro]

equality can be whatever you like, this is just a mechanism for automatically supplying typing proofs from the context where needed

[Mario Carneiro]

it depends on the type of x and y

[Steven Obua]

But if x is a nat, it is also a real

[Mario Carneiro]

that's fine, if x is a nat then it's plus_nat

[Mario Carneiro]

it's a convenient bit of data entry, it's plus_nat under the hood

[Mario Carneiro]

the user can write plus_real x y if they really need to, or reconsider x : Real or whatever the notation is

[Steven Obua]

I don't like it.

[Steven Obua]

It is OK to dispatch based on type.

[Steven Obua]

so, + can dispatch to "Type.plus"

[Mario Carneiro]

As long as the functions agree on the common domain it shouldn't matter which is which

[Steven Obua]

It shouldn't, but who ensures that?

[Mario Carneiro]

The user

[Steven Obua]

But that means that the user can mess up the system badly.

[Mario Carneiro]

I think what I described is basically what lean will do as well, with a combination of typeclass inference and coercion

[Mario Carneiro]

sure, but there is definitely nothing you can do about that

[Steven Obua]

No, in Practal, the user will have to prove that it is compatible with subtyping.

[Mario Carneiro]

you can still screw up lots of other things

[Steven Obua]

Yeah, but this is one thing I can do something about

[Steven Obua]

And it makes sense.

[Mario Carneiro]

It's not necessarily desirable

[Steven Obua]

Real.plus should be the same as Nat.plus on Nat.

[Mario Carneiro]

one could have such a thing in lean as well but it's not desirable

[Steven Obua]

Why not?

[Steven Obua]

It is desirable if you have subtyping.

[Mario Carneiro]

some coercions aren't compatible with operators

[Mario Carneiro]

some are only compatible with some operators

[Steven Obua]

That's why coercions are different from subtypes.

[Steven Obua]

Not a problem, but as far as subtyping is concerned, you want it to be the same.

[Mario Carneiro]

for example \u x + \u y = \u (x + y) holds for the nat -> int coercion but \u x - \u y = \u (x - y) doesn't

[Mario Carneiro]

For the fin n -> nat coercion \u x + \u y = \u (x + y) doesn't hold

[Mario Carneiro]

that one is probably traditionally a subtype

[Mario Carneiro]

it's even literally a subtype in lean

[Steven Obua]

fin n?

[Mario Carneiro]

{0,...,n-1}

[Mario Carneiro]

addition on fin n is as in Z/nZ

[Steven Obua]

Well, it would not be a subtype in Practal, but a whole new type

[Mario Carneiro]

the coercion is still useful though

[Steven Obua]

Definitely.

[Steven Obua]

As I said, I would want coercions in Practal as well!

[Mario Carneiro]

If you have coercions then why not lean on them and forget literal subtyping?

[Steven Obua]

Because subtyping is too good to have! As I said, if you have type extensionality, you getn subtyping automatically. And type extensionality is at the core of my approach.

[Mario Carneiro]

I wonder whether you could have coercions and subtype coercions in the frontend, with the latter lowering to literal subtyping

[Mario Carneiro]

that way you can have type inference where x : nat and \u x : real, but without the headache of \u x + \u y = \u (x + y) lemmas

[Mario Carneiro]

because subtype coercions commute with everything by definition (because they are literally nothing to the kernel)

[Steven Obua]

I am not sure what "subtype coercions" would get you.

[Mario Carneiro]

they let the user direct the type checker, which, recall, is a mechanism for inserting typing proofs where required

[Steven Obua]

But there is no type checker.

[Mario Carneiro]

so in a certain context you have x : nat because for example you were proving \forall x : nat, ... and intro'd x, and now the typechecker keeps track of x : nat and when it needs to prove x + x : nat it uses this fact; and then the user can talk about \u x : real and the typechecker knows that the coercion nat -> real exists so that this typechecks

[Mario Carneiro]

but under the hood that's really a theorem nat <= real

[Steven Obua]

But why would the user talk about \u x : real ?

[Mario Carneiro]

actually they would probably write x : real and the frontend would insert the \u (and the backend would take it out again)

[Mario Carneiro]

or they would apply x to a real function

[Steven Obua]

Well, I think we can agree that coercions can come in handy. But when the types in questions are already subtypes, they don't make sense.

[Mario Carneiro]

you might wonder why to go around in circles like this but the advantage is that you can handle true coercions in exactly the same way

[Steven Obua]

Maybe you want to embed Nat into Real in a different way . Then you need coercions.

[Steven Obua]

No, the point is that you can handle subtyping much better than coercing.

[Mario Carneiro]

and also having the \u in there means that you get stable answers to what the type of a thing is, which is important for stuff like typeclass inference

[Steven Obua]

Why would you want to make subtyping as bad as coercions? That's kind of besides the point.

[Mario Carneiro]

Why not ensure that subtyping coercions are as good as literal subtyping? Then it doesn't matter

[Steven Obua]

Because they cannot be.

[Mario Carneiro]

how so

[Steven Obua]

Coercions can never be as good as subtyping. At least that's what I believe. They are just simpler, conceptually.

[Mario Carneiro]

subtyping coercions are frontend magic around literal subtyping, so it should be possible to make them just as good in practice

[Steven Obua]

They don't always apply though. And that's when coercions come in.

[Mario Carneiro]

this is just an implementation trick to make sure the typechecker remains usable

[Mario Carneiro]

the typechecker that practal doesn't have

[Steven Obua]

There is no type checker.

[Steven Obua]

:-)

[Mac]

Mario Carneiro said:

Why not ensure that subtyping coercions are as good as literal subtyping? Then it doesn't matter

If I may, I will jump into this dialogue. I agree with @Steven Obua that coercions are, in general, bad. I would argue they are largely an artifact of the types being (usually)represented as tagged unions and thus the coercion allows the compiler to have a point where it can switched between tags. When possible, I would always prefer subtypes, supertypes, and unions. In fact, this is one of the reasons why I consider TypeScript to be the language with the best type system on the market.

[Mac]

On the other hand, I disagree with @Steven Obua on the following claim:

Steven Obua said:

I would say programmers are more "syntax" based.

I would argue programmers are much more "semantic" than "syntax" in how they view types and computer languages in general. I would also say mathematics is much more "syntactic".

Mathematical logic is essentially just a complex rewrite system (at least from a proof theory perspective) -- and rewrite systems are about as syntactic in nature as you can get. Furthermore, to the due to abstract nature of math, the logic itself rarely has meaning beyond the syntactic at the level being discussed (even if the concepts do have concrete parallels) .

Programmatic logic, however, often deals entirely with the semantic meaning of programs. This is why imperative programming is the natural default and functional programming is a novel foreign concept (whereas the opposite is true for math).

[Steven Obua]

Yeah, don't take my "semantic / syntactic" statement too serious. I think you also have to distinguish between various types of logicians, and normal mathematicians.

[Steven Obua]

Certain types of logicians, in particular some proof theorists, are all about syntax. I guess that is part of their job description. But that is not how mathematics in general works.

[Steven Obua]

So, when I said "programmers are more syntax based", that was really too general a statement.

[Steven Obua]

By the way, I agree with your comment about Typescript. I looked at how Typescript uses types, and some of it made a lot of sense to me, and influenced Practical Types.

[Mac]

Steven Obua said:

Yeah, don't take my "semantic / syntactic" statement too seriously. I think you also have to distinguish between various types of logicians, and normal mathematicians.

Fair enough.

Steven Obua said:

Certain types of logicians, in particular some proof theorists, are all about syntax. I guess that is part of their job description. But that is not how mathematics in general works.

I think this probably depends on what one consider to be "syntax". As a person who ascribes to formalist philosophy of mathematics, I personally would consider all of mathematics to be about "syntax" . However, this is problem because I view a lot more things as "syntax" than a lot of people I have encountered.

[Kevin Buzzard]

Steven Obua said:

Maybe you want to embed Nat into Real in a different way .

This is just the sort of thing which mathematicians see computer scientists writing and think "??"

There is only one map from Nat into Real which deserves to be called a coercion. You know it's a coercion because when it's used in mathematics papers there is no notation used for it. This is an important thing for mathematicians because they do not think about mathematics completely type-theoretically -- they use a hybrid system. For mathematicians Nat is a subset of Real, and the coercion is the inclusion, and this remains true whatever your foundations are. We're using dependent type theory here so it's important for mathematicians to make this map invisible to the user even though it exists in type theory.

Of course we're interested in other maps from Nat to Real, but we call them things like f and not "the coercion".

[Mac]

Kevin Buzzard said:

You know it's a coercion because when it's used in mathematics papers there is no notation used for it. [...] For mathematicians Nat is a subset of Real, and the coercion is the inclusion, and this remains true whatever your foundations are.

While I largely agree with your point, I would argue that the fact there is is no notation for it implies it should not, ideally, be a coercion. In math a 'Nat' is a 'Real', there is no translation occurring. Thus, ideally, there would be no coercion. The idea this even amounts to a coercion is an artifact of the implementation (and to a lesser extent, the type theory), not a part of mathematical logic.

However, by your statement that 'the coercion is the inclusion', I suspect you may have a different concept of what a 'coercion' is. I, as a computer scientist, view a coercion as the process of translating one data type to another. Generally, this comes with conceptual rule that the what the input and output abstractly represent is equivalent in some manner. Due to the 'in some manner', there can be causes where multiple valid coercions exists. For example, if I wish to coerce a Bool to a UInt32, one valid coercion might be to coerce false to 0 and true to 1. Another valid coercion might be to coerce false to 0 and true to 0xFFFF (all ones). Thus, in general, there is often no 'right' coercion. Cases where there is a 'right' coercion (ex. Nat/Real) should usually ideally not really be coercions. At least, that is how I view the concept of 'coercion'.

[Mario Carneiro]

While I largely agree with your point, I would argue that the fact there is is no notation for it implies it should not, ideally, be a coercion. In math a 'Nat' is a 'Real', there is no translation occurring. Thus, ideally, there would be no coercion. The idea this even amounts to a coercion is an artifact of the implementation (and to a lesser extent, the type theory), not a part of mathematical logic.

I don't think that this actually works though, as a litmus test for coercions that should be inclusions, since generally the elements of Z/nZ are written as unadorned numbers despite the fact that the quotient map Z -> Z/nZ is not an injection, so there is no hope of making this be the inclusion map

[Mario Carneiro]

In fact, I would say that the lack of any notation for the function is the characteristic property of a coercion. Certainly that's the way it manifests in lean

[Mac]

Mario Carneiro said:

since generally the elements of Z/nZ are written as unadorned numbers despite the fact that the quotient map Z -> Z/nZ is not an injection, so there is no hope of making this be the inclusion map

When you say unadorned numbers do you mean numerals or something else? Because numerals are notation, they are not elements of a type (in my view). Their meaning is based on context (i.e., in type theory, the expected type of the value). Thus, unadorned numerals can be part of any type without coercion.

[Mario Carneiro]

Numerals most commonly, but also sometimes elements of nat. Whether notation is used here (for example writing [n] or something) seems to be context-dependent

[Mario Carneiro]

I can't really think of any situation where a mathematician would be okay with writing 37 in a given type but not n where n is indicated to be an arbitrary natural number

[Mac]

@Mario Carneiro I would be very concerned about any formal writing where you explicitly indicate n is to represent a natural number but then use it in places where it is implicitly coerced into something else (especially in a non-reversible manner) without any notation.

[Mac]

However, one part of this still has me confused. Is there even a mathematical notion of coercion? I tend to think of type coercion as a concept original to computer science. And there is certainly both explicit and implicit notions of type coercion in computer science.

[Mac]

For example, in Lean, type ascriptions are a form of explicit type conversion that can take the form of a cast or a coercion.

[Mario Carneiro]

You should ask a mathematician for more attestation of coercions, but here are some examples that come to mind:

• Using $nx$ in the definition of an archimedean field
• Using $n$ and $\omega^n$ as ordinals
• Using $n$, $\aleph_n$ as cardinals
• Using $n$ as a surreal number
• Using $a$ or $aI$ as a matrix where $a$ comes from the scalar ring
• Using $n$ or $[n]$ as an element of $\Bbb Z/k\Bbb Z$, as mentioned
• Using $a$ as an element of $\Bbb R^1$, where $a$ is a real number
• Using $(a, b)$ as an element of $\Bbb R^2$, where $a, b$ are real numbers
• Using $x \in E$ as an element of $F$ in a field extension $E\subseteq F$
• Using $X$ as an element of the polynomial ring $R[X]$

[Mario Carneiro]

In most cases, this can be explained as "mathematician decides that a certain subset relation holds because it is convenient in the moment, so that the coercion function is the inclusion". The issue is that these subset relations are not globally coherent

[Steven Obua]

Using $x \in E$ as an element of $F$ in a field extension $E\subseteq F$

Why are these subset / subtype relations not globally coherent? For example, in Practal
$E \subseteq F$ would actually hold, I believe, so no need for a coercion. Same for polynomial ring, $R^1$, scalar/ring, etc.

$\Bbb Z/k\Bbb Z$ is different, here indeed a subtype relation cannot work because an operator like $+$ has a different meaning. But you gave the notation yourself, in this case one often uses $[n]$ as a notation, so again, no coercion needed, as $[\cdot]$ does the mapping explicitly.

In general, in cases where a coercion is more than just a subtype inclusion, mathematicians don't have a problem of using a bit of explicit notation instead of a coercion.

[Eric Wieser]

Would a mathematician draw the distinction between aI being a coercion (↑a * I) and not just a heterogeneous multiplication (a • I)?

[Steven Obua]

I would think a heterogeneous multiplication feels more natural. Really, I don't think mathematicians use coercions at all, just subtypes. Coercions are a workaround for type theorists because they cannot deal with subtypes.

[Steven Obua]

Here is an example of a typical way to construct a new "type", as it is planned for Practal:

typedef ℤ = ℕ ⨯ ℕ
  identify (a, b) with (c, d) where a + d = c + b
  identify n in ℕ with (n, 0)

This is impossible in any current ITP system. It is a trivial and common construction for mathematicians. And it will be easy for Practal. You get a subtyping relation ℕ ⊆ ℤ, in a natural way. Nobody would think of this relation in terms of coercions.

An ITP system that cannot do above construction is just not adequate for mathematics, no matter how "constructive" it is otherwise. It will always be a pain to use it, even though workarounds are possible, of course.

[Kevin Buzzard]

I can assure you that if v is an element of a vector space over a finite field and n is a natural then a mathematician would write none of n • v, n * v, \u n • v... but would instead always write $nv$.

[Kevin Buzzard]

Similarly if n were in a ring and v was in a module for some algebra for that ring (for example a real number acting on a complex vector or on a module for a ring of real-valued functions)

[Kevin Buzzard]

It would not even occur to the mathematician that something needed to be said here

[Eric Wieser]

identify n in ℕ with (n, 0) sure looks a lot like the lean coercion coe := λ n : ℕ, (n, 0) to me. Sure, you've used the same keyword you're using for quotient types to make it not look like that, but I find it hard to believe those two identify lines have particularly similar semantics

[Steven Obua]

They have pretty much the same semantics, they both define what equality in the newly created type looks like.
Here is another example:

typedef ℚ = ℤ ⨯ (ℤ \ {0})
  identify (a, b) in ℚ with (c, d) in ℚ where a ⋅ d = c ⋅ b
  identify z in ℤ with (z, 1) in ℚ

This time I didn't leave out the in clauses that are trivial.

In Lean, it is just a coercion. In Practal, it is what elements of ℤ (respectively ℚ) ARE.

[Steven Obua]

That is why you have to do it at the point of creation of the respective types. You cannot tag that on later, as with coercions.

[Eric Wieser]

What happens if you add something that doesn't commute with previous identifys like identify n in ℕ with (1, n) in ℚ to that definition?

[Steven Obua]

Of course you have to prove that the identifies are compatible with each other. If it can be done automatically, it doesn't need to be visible. If it cannot be done automatically at the moment, but is still trivial, it can be hidden from the casual reader of the construction and shown on request. If the proof of compatibility is interesting in itself, you would show it by default, I guess.

[Eric Wieser]

What precisely does it mean to prove identifys are compatible? Presumably in the context of proving that, you don't actually have the identifies "active", and are proving things about explicit coercion functions?

[Steven Obua]

Because Practal doesn't have a static type system, but typing judgements are just normal theorems, I expect stuff like this to be straightforward to implement. The burden is of course on providing the necessary proofs, but I am betting on strong automation here.

[Steven Obua]

Yes, you will be talking about mappings between types.

[Steven Obua]

Even without strong automation, it is better that I can actually do the construction I want to do, with a little bit of computer-assisted leg work to prove it correct.

[Steven Obua]

Instead, currently people are told that they shouldn't be using certain constructions of integrals, for example. How utterly ridiculous is that?

[Steven Obua]

I have not worked out in detail yet which proof obligations would be generated. But it should work along these lines:

• First an equivalence relation $\sim$ on the representation $R$ of the new type is generated from those identifications entirely defined on the representation; here no inconsistency can occur, just the equivalence classes can be bigger than what you would expect if you do something wrong.
• Then, for each identification mapping $I_N : N \rightarrow R$ from a different type $N$ into the representation $R$ of the new type it must be shown that equality on $N$ is equivalent to equality according to the equivalence relation on the image $I_N(N)$ of $N$, i.e. $\forall u\, v : N. (u = v) = (I_N(u) \sim I_N(v))$
• Finally, if we have done this for multiple types $N_1, \ldots, N_k$, we need to prove that on the pairwise intersections of the images of the $N_i$ the mappings are compatible with the original equality relationship between the $N_i$:
  $\forall i\, j. \forall u : N_i. \forall v : N_j. (I_{N_i}(u) \sim I_{N_j}(v)) = (u = v)$

If all these conditions can be proven, the new type can be created.

[Steven Obua]

For your suggested mapping of $(1, n)$, this would not work from the start, as $0$ cannot be represented in R = ℤ ⨯ ℤ \ {0}.

But if we mapped not ℕ, but ℕ \ {0}, then this would be fine. The third condition is not relevant, as there is only one other type injected into ℚ. And the second condition holds, as $n = m$ must mean $(1, n) \sim (1, m)$, which is equivalent to $m = n$.

Now, if you start defining addition on ℚ, you will want to ensure that it is compatible with addition on all of its subtypes, which is where you will run into problems here. I haven't worked out yet in detail how overloading should work in the presence of subtypes.

[Steven Obua]

Oh I just saw that you wanted your mapping in addition to the previous one. That would then clash because of the third condition.

[Mario Carneiro]

Steven Obua said:

Using $x \in E$ as an element of $F$ in a field extension $E\subseteq F$

Why are these subset / subtype relations not globally coherent? For example, in Practal
$E \subseteq F$ would actually hold, I believe, so no need for a coercion. Same for polynomial ring, $R^1$, scalar/ring, etc.

My contention is that the mathematician isn't thinking of them as being globally coherent, whether or not they actually are. So even if you try to make them so and pop up proof obligations to ensure it is consistent, the proof obligations will seem weird and unmotivated, and contribute to the usual complaint of "formalization isn't like regular mathematics".

The examples I gave of "coercions" may or may not actually be realized as coercions in a proof assistant. For example, as Eric mentions, we do $nx$ using scalar actions in mathlib instead of any kind of coercion. Additionally, some are at least apparently "true subtypes", like the $E\subseteq F$ example - this one gives that away right in the notation. It's hard to gather evidence on this without picking the brains of mathematicians that use the notation, but I think that even these "true subtyping" relations are only meant to hold by some kind of abuse of notation, because the actual mechanism needed to make it hold, by cutting out a piece of the newly constructed field extension $F$ to make room for $E$, is far too troublesome to countenance in informal maths.

[Mario Carneiro]

I'm curious how you intend to make $R\subseteq R^1$ hold in practal.

[Mario Carneiro]

You will certainly have trouble with $R^3=R\times R^2=R^2\times R$, since $\pi_1(1,2,3)$ (where $\pi_1:A\times B\to A$ is the pairing projection) depends on which one you choose

[Mario Carneiro]

These identifications may be done with a comment that acknowledges the coercion, for example "viewing $R^{m+n}$ as $R^m\times R^n$, ... $(u, v)$ where $u\in R^m$ and $v\in R^n$, ...". I would argue that the "viewing" clause is saying "let's assume this coercion exists for the purpose of this proof", and it will not be explicitly notated, but there is no intent for the coercion to be globally coherent and a proof obligation to show it is would be undesirable

[Steven Obua]

$R^1 = R, R^{n+1} = R^n \times R$

Then $P(R) = \bigcup_{n=1}^\infty R^i$.

[Steven Obua]

That's how I would do it.

[Steven Obua]

As for how to extend $E$ to $F$, see my examples above with ℕ, ℤ and ℚ. No cutting out required, just proving sensible compatibility conditions. And EVERY mathematician does these proofs, it's just that they are so obvious usually they can be skipped. This is just how it would be in Practal as well.

[Mario Carneiro]

Steven Obua said:

That's how I would do it.

Of course it's possible to just make a choice and stick with it, this is what all existing formal systems do in the first place. My point is that the mathematician wants to avoid making such commitments, so that they can pretend they made the convenient choice when it comes up later in a proof

[Steven Obua]

I don't think any mathematician is particularly worried about that choice. If you just stick to it, no problems will arise. If for some reason you cannot stick to it in a particular situation, well, there is something more to explain here then.

[Reid Barton]

So does $R^0 \times R = R^{0+1} = R^1 = R$?

[Florian Rabe]

@Steven Obua I've looked over PractTal. How would you handle quotient types?

[Steven Obua]

@Reid Barton Depends on what you want to do, I guess. Let's say you have a List(R) type already. As it is just a data structure, you will NOT want R ⊆ List(R) by design. But if you want to use it to model polynomials, you can define this:

typedef P(R) = List(R)
  identify r in R with [r]

You can then go on and define

typealias R^i = { p : P(R) | length p = i }

You should then be able to define ⨯ on P(R) so that your equation holds.

I am not sure if the above leads to problems, because now R = R^1 = (R^1)^1 etc. Sounds reasonable, but maybe there is a problem here somewhere.

[Steven Obua]

@Florian Rabe , see the examples above from https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/Practical.20Types/near/247901385 on

[Florian Rabe]

Steven Obua said:

Florian Rabe , see the examples above from https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/Practical.20Types/near/247901385 on

Ah, so every type comes with its own equality, which can be used for quotienting.
Could you have a look at my paper on Type-Dependent Equality (https://kwarc.info/people/frabe/Research/rabe_tde_21.pdf) and explain how Practal handles the rule for substitution?

[Mario Carneiro]

@Steven Obua With that definition of P(R), I think you don't have List(R) ⊆ P(R) or some similar thing, so { p : P(R) | length p = i } doesn't typecheck, assuming that length is a function defined on List(R). In fact, you can't have List(R) ⊆ P(R) because P(R) adds some identifications that aren't true in List(R).

[Steven Obua]

@Florian Rabe The problem of inconsistency is handled in Practal by making sure that there is only one equality. So, you could call it type dependent, but at the same time it is not, because there is only one equality.

[Steven Obua]

There are the initial types of propositions, types, natural numbers and function spaces. They don't intersect, so there is no problem caused by pairs of types. There can only be problems within a type, and I have been careful to avoid them. For example, function spaces are only in a subtyping relationship if they have the same domain.

[Mario Carneiro]

More than the base types, I think the interesting thing going on here is where typedefs come from and how they manage to have all the identifications you ask for

[Steven Obua]

Note that equality in Practal does not take an additional type parameter, it is just A = B, without any hidden type annotations etc.

[Steven Obua]

@Mario Carneiro Yes, I think so too. The conditions I have stated earlier should do the job, so applying that to the List example should show a problem if there is one.

[Steven Obua]

That is why it is crucial that all the glueing happens at type creation time.

[Mario Carneiro]

That doesn't answer the question about how length p works without a coercion though

[Mario Carneiro]

what are the introduction and elimination principles for typedef?

[Steven Obua]

@Mario Carneiro Yes, the length definition is the problem. I would like to say something along the lines of length(rep p) instead, but I guess it has to be length(rep R p) instead or something.

[Steven Obua]

typedef should introduce rep and abs functions after a successful definition, similar to HOL. How exactly that would work, I haven't thought about yet.

[Mario Carneiro]

I think it has to be rep[P(R)] p or something that picks out precisely which typedef rep you want, because p could have a type that doesn't have anything to do with it, like p : R due to your identification

[Mario Carneiro]

In HOL the type definition command itself will give you new rep and abs functions that you have an opportunity to name

[Steven Obua]

Basically, rep and abs are overloaded functions, and as I said, I don't know the interplay between overloading and subtyping. Could be that it is easy to solve, could be that a serious problem hides here.

[Mario Carneiro]

rep can't be an overloaded function because it takes conflicting values on different typedefs

[Steven Obua]

Each typedef creates a new type, so why would they be conflicting?

[Mario Carneiro]

because rep maps from a type not under your control

[Mario Carneiro]

abs can probably be an overloaded function, but not rep

[Mario Carneiro]

but abs is mathematically unnatural anyway

[Steven Obua]

Ok, so there is one function mapping from the new type T to the representing type R, in symbols T → R. What do we call this function?

[Steven Obua]

I am calling it rep

[Mario Carneiro]

That's abs

[Mario Carneiro]

rep maps into the new type IIRC

[Steven Obua]

I find it more intuitive the other way around, but OK

[Mario Carneiro]

I find them both unintuitive, I might have them mixed up

[Mario Carneiro]

lean has quot.mk and quot.lift

[Mario Carneiro]

quot.mk : A -> A/r and quot.lift : (A -> B) -> conditions -> (A/r -> B)

[Mario Carneiro]

people tell me lift isn't the right word either though

[Mario Carneiro]

but notice that quot.lift is not simply A/r -> A. That's the map I call unnatural

[Steven Obua]

let me check hol light for the naming

[Mario Carneiro]

abs goes into the new type and rep maps back out in HOL

[Mario Carneiro]

but HOL uses it for subtypes instead of quotients, so some of the polarity is switched

[Steven Obua]

yes, just checked, so that makes sense. Because rep maps to the representing type, and abs abstracts to the new type

[Steven Obua]

No, the polarity is the same. There is nothing special about quotient types here in that sense.

[Mario Carneiro]

quotient maps are defined by a universal property involving a map into the new type, while subtypes are defined by a universal property involving a map out of it

[Mario Carneiro]

because quotient types are equalizers and subtypes are coequalizers

[Steven Obua]

Well, maybe in category theory.

[Steven Obua]

Not in Practal.

[Mario Carneiro]

in mathematics

[Mario Carneiro]

if you have something that isn't isomorphic to that it's not a quotient type

[Steven Obua]

Identify just glues things together. I don't see why "polarity" or anything like that comes into play.

[Mario Carneiro]

The map into your quotient is easy. That's what lean calls quot.mk, and it's like the function List(R) -> P(R) in your example

[Mario Carneiro]

the hard part is mapping out of the type, because you have to respect all that gluing you did

[Steven Obua]

Yes, like I said: rep is an overloaded function, and how do you define it safely in the presence of subtyping?

[Steven Obua]

I think if you have a solution for that general problem, you have the solution for typedef

[Mario Carneiro]

Consider:

typedef Foo = Nat
  identify 0 with 1
typedef Bar = Nat
  identify 1 with 2

Now rep 0 : Foo and rep 0 : Bar, so in particular rep 0 = rep 1 : Bar which seems bad

[Mario Carneiro]

without knowing what the rules are for elimination from a typedef I can't derive a contradiction from this but it seems fishy

[Steven Obua]

So first we should get the names straight :-)

[Steven Obua]

I think you mean abs 0 : Foo and abs 0 : Bar

[Mario Carneiro]

I prefer mk

[Steven Obua]

And the abs function is of course dependent on the type, so there would be abs_Foo, and abs_Bar.

[Steven Obua]

I don't. Let's take rep and abs.

[Mario Carneiro]

what even is rep in this example?

[Mario Carneiro]

abs is sort of already taken in mathematics

[Steven Obua]

And also, probably helpful to not get overloading into this, it probably doesn't play a role after all.

[Steven Obua]

Ok, then represent and abstract

[Mario Carneiro]

lean uses mk consistently for constructors of inductive types, quotient types and other "new" types

[Steven Obua]

So after your definitions, we have functions represent_Foo and abstract_Foo and represent_Bar and abstract_Bar

[Steven Obua]

So if mk is abs, what is rep ?

[Mario Carneiro]

honestly spelling the names out doesn't help me at all

[Mario Carneiro]

there is no rep

[Steven Obua]

exactly

[Mario Carneiro]

no I mean it doesn't make any sense to have in the first place

[Mario Carneiro]

like I said, what is it in this example?

[Steven Obua]

But in our context it makes a lot of sense.

[Steven Obua]

Ok, I call it rep_Foo, rep_Bar, abs_Foo and abs_Bar

[Mario Carneiro]

Do you have empty types?

[Steven Obua]

Yes.

[Mario Carneiro]

If so, you can't have a rep

[Steven Obua]

You mean for an empty type you cannot have a rep.

[Mario Carneiro]

yes

[Mario Carneiro]

and for nonempty types it's always going to be arbitrary, for example is rep_Foo (abs_Foo 0) equal to 0 or 1

[Steven Obua]

Yes, so I guess a good proof obligation is to show that it is not empty. Makes a lot of sense, because otherwise the new type would be equal to the empty type due to type extensionality

[Steven Obua]

So, let's assume our new types are not empty from now on.

[Mario Carneiro]

That sounds like an unnecessary thing to worry about, and a limitation that will add unnatural proof obligations

[Mario Carneiro]

there are lots of type families that are not necessarily nonempty

[Mario Carneiro]

don't go the mizar route

[Mario Carneiro]

this is why lift is better than rep

[Steven Obua]

So, in your case, rep_Foo : Foo → ℕ, abs_Foo : ℕ → Foo, rep_Bar : Bar → ℕ and abs_Bar : ℕ → Bar.

[Steven Obua]

Forget about lift and so on. It's different.

[Mario Carneiro]

what are the axioms for those functions?

[Steven Obua]

And there is no problem with making a special case for the empty type. It even makes a lot of sense, as I explained.

[Steven Obua]

What would you think the axioms are?

[Mario Carneiro]

I know what the axioms for lift are, but for rep you have a symmetry breaking problem

[Steven Obua]

:rolling_on_the_floor_laughing: I don't know, does HOL Light also have a symmetry breaking problem?

[Mario Carneiro]

HOL light isn't doing quotient types

[Mario Carneiro]

you are

[Steven Obua]

You are in your Foo / Bar example also not doing quotient types

[Steven Obua]

So maybe just forget about "quotient types"

[Mario Carneiro]

yeah, that's a quotient of nat making 0 = 1

[Steven Obua]

That's glueing 0 together with 1.

[Mario Carneiro]

that's called a quotient type

[Mario Carneiro]

importantly, 2 and 3 are not equal in Foo

[Mario Carneiro]

that is, elements are equal only if they were "glued" or if they follow from equality axioms from gluing prescriptions

[Mario Carneiro]

that's a quotient type

[Steven Obua]

As I said, let's not use the word "quotient type". It seems to have a certain meaning to you, and not all of them apply in our case, I think.

[Mario Carneiro]

To define a function on Foo -> A, you give a function f : Nat -> A such that f 0 = f 1

[Mario Carneiro]

and the resulting function lift f : Foo -> A will satisfy lift f (abs n) = f n

[Steven Obua]

Yes, let's talk about how to define functions on Foo.

[Mario Carneiro]

no need for rep

[Steven Obua]

To define f : Foo → A, I want to do it by defining g : ℕ → A first, and then set f x = g(rep x)

[Steven Obua]

So you see, there is a rep in here, or rather rep_Foo

[Steven Obua]

let' say that a ~ b in ℕ if a and b are glued together by abs_Foo

[Steven Obua]

We might have x ≠ y, but abs_Foo x = abs_Foo y. So we need g(x) = g(y) for abs_Foo x = abs_Foo y, I guess.

[Steven Obua]

So that's the condition on g we need to make f well-defined.

[Mario Carneiro]

right, that's exactly the condition on lift that I mentioned

[Steven Obua]

It doesn't help to switch names all the time. Let's stick with rep and abs.

[Mario Carneiro]

lift has a different type signature than rep

[Steven Obua]

What is it?

[Mario Carneiro]

lift : (OldType -> A) -> conditions -> (NewType -> A)

[Mario Carneiro]

if you don't use dependent types then the conditions are not actually arguments to the function

[Mario Carneiro]

so it would just be lift_Foo : (Nat -> A) -> (Foo -> A) in this example

[Mario Carneiro]

you probably need A to be an additional argument, it's a family of functions over any target type A

[Steven Obua]

So lift is about how to go from functions on OldType to functions on NewType. But rep and abs are more basic. They are about going from members of OldType to members of NewType

[Steven Obua]

lift can then be defined in terms of those.

[Mario Carneiro]

yes, and I assert that's the wrong way to think about quotient types

[Steven Obua]

It might be a way you don't like. Doesn't mean its wrong.

[Mario Carneiro]

I have never seen any presentation of quotient types that prefers that approach outside of formalization (and HOL in particular)

[Mario Carneiro]

it's almost always about the quotient map and the "well definedness condition"

[Steven Obua]

You have never seen an approach like Practal either. It's the best though :-)

[Steven Obua]

In the end, I think rep and abs is conceptually simpler.

[Steven Obua]

It is simpler to talk about members of types, than about functions on types. At least for me.

[Steven Obua]

So I'll stick to that terminology for now, to understand why the List example is problematic.

[Mario Carneiro]

So what are the proof obligations for the P(R) example?

[Steven Obua]

I'll think about the problem offline for now, gotta eat :-) I'll post later if I have something!

[Mac]

Mario Carneiro said:

lean uses mk consistently for constructors of inductive types, quotient types and other "new" types

I quite dislike Lean's use of mk. The word 'mk' (i.e. 'make') is very imperative and I associate that strongly with a side-effect having action (i.e. a monadic action) and yet most mk functions are pure. This, to me, is very counterintuitive.

[Mac]

Mario Carneiro said:

and for nonempty types it's always going to be arbitrary, for example is rep_Foo (abs_Foo 0) equal to 0 or 1

Wouldn't it definitely be 0? I mean the whole idea is that abs abstracts from a primitive type to an abstract typedef and rep converts the abstract typdef back to its primitive type representation, right? So rep . abs = id should always hold?

[Mac]

I would also suggest the shorthand repr and abst for rep and abs to prevent the name clash with math's abs.

[Eric Wieser]

I think Mario's point is that abs_Foo 0 = abs_Foo 1, so by substitution we would assume rep_Foo (abs_Foo 0) = rep_Foo (abs_Foo 1). If you pick rep_Foo (abs_Foo 0) = 0 you can't also pick rep_Foo (abs_Foo 1) = 1, because if you did you no longer have x = y → f x = f y.

[Eric Wieser]

Lean resolves this by having both docs#quot.unquot, which satisfies unquot (mk x) = x but lives in unsound meta land, and docs#quot.out which only satisfies mk (out q) = q and is noncomputable

[Steven Obua]

I've been thinking about it for a bit now, and I think the best strategy is to just implement it in Practal Light. That should clarify problems with this typedef approach if there are any. There will be a better basis for discussion then, and the proof obligations will be clear then. From what I see currently, typedef that defines a type without parameters works fine as described, including quotients and injected subtypes. For a typedef that takes a parameter, as in Poly X, which has parameter X, there are (at least) two options what that can mean, even without any quotient or injecting features. It can be a "disjoint" typedef, where each different X yields a different type, that is X ≠ Y ⟶ Poly X ∩ Poly Y = ∅. This case should be similar to the parameterless case, just that everything takes a parameter X in addition. Or it can be a "union" typedef , where equal representations imply equal abstractions regardless of parameter:
r : Repr[X] ∩ Repr[Y] ⟶ abstr X r = abstr Y r.
I think both options make sense.

[Florian Rabe]

@Steven Obua @Mario Carneiro regarding Quotient types and abs/rep:

I didn't follow all the discussion, but the following might be helpful.
The abs/rep intuition from HOL-style predicate subtypes carries over to quotient types as follows:

For predicate types
abs: newtype -> oldtype is the canonical injection
rep: oldtype -> newtype is a partial function (undefined for values not in the subtype)

For quotient types
abs: newtype -> oldtype is a non-deterministic function (returns any element of the equivalence class)
rep: oldtype -> newtype is the canonical projection

You can unify the two by using a total, injective relation
r : newtype x oldtype -> prop
r is functional for a subtype, surjective for a quotient type, and both functional and surjective for an isomorphism.

[Steven Obua]

@Florian Rabe Hah, you also got rep and abs the wrong way around :-)

[Florian Rabe]

Steven Obua said:

Florian Rabe Hah, you also got rep and abs the wrong way around :-)

Seriously? I checked back and forth like 5 times before I gave up :)

[Mac]

I really am surprised at how confusing rep and abs seem to be. Could someone explain what makes the terminology confusing to them? I would really like to know were the counterintuition lies since the terms seem rather intuitive to me.

[Mario Carneiro]

"abstraction" is not helpful because I'm not sure which side is considered to be more abstract, and "representation" sounds like it might be the map into the new type but apparently it's the other way around

[Mac]

@Mario Carneiro Interesting. It thus appears we have very different notions of 'abstract' and 'representation'. In my view, the if type A is defined in terms of type B (ex. typdef A = B), I would always describe A as more 'abstract than B`. And I view the 'representation' of an 'abstract' type to be said definition. I feel like this close to the usual CS definitions of those words. Could it be that 'abstract' and 'representation' have very different intuitions in math vs CS?

[Mario Carneiro]

I can see why you might call A more abstract than B, but it still seems categorically wrong to talk about the constructor of an (abstract) data type as "abstraction"

[Mario Carneiro]

abstraction is the meta-level mechanism of introducing A as a type

[Mario Carneiro]

but the constructor is just a constructor

[Mario Carneiro]

which is why I prefer names like new or mk or of or intro

[Mario Carneiro]

similarly, the reverse map is a destructor or (field) projection, so I would prefer a name like dest or out or proj

[Mac]

@Mario Carneiro Interesting, it seems we have very different views on terminology.

First, I have long had mixed feelings about the terms 'constructor' and 'destructor' being used to describe the manipulation of pure terms, as I associate those terms with imperative impure actions. However, there are admittedly many cases where no better term exists. (Luckily, as far as I am concerned, this is not one of those cases! :stuck_out_tongue_wink:)

Also, as an aside, I do not get where the term 'projection' for dot notation (or destructors) came from -- I suspect math -- but it strikes me as wholly unintuitive jargon. Admittedly, the term 'field' for such things does seem natural to me, despite the fact that it is also jargon from I am not sure where).

On the other hand, it seems perfectly natural to me to define as 'abstraction' the operation of producing some 'newtype from some 'oldtype', or as I would phrase it: (further) abstracting 'oldtype' to 'newtype'..

[Mac]

I suspect this may all came down to the natural jargon of someone coming from a primarily computer science background vs. the natural jargon of someone coming from a more math-focused background (if I am correct in assuming your background) .

[Steven Obua]

Maybe just call the functions new and old :-)

[Mario Carneiro]

@Mac

First, I have long had mixed feelings about the terms 'constructor' and 'destructor' being used to describe the manipulation of pure terms, as I associate those terms with imperative impure actions.

Constructors in lean are a very direct analogue to constructors in java or rust. Constructors in non-functional languages can have side effects, but, well, so can everything else. Rust in particular uses new as a conventional function name for a function returning the new type and calls it a constructor, even if it is a pure function (and it usually is), and at the memory level lean's constructor is allocating memory and filling it with provided stuff, so I don't think it is a misnomer at all.

An alternative view point from formal logic is to call this the "introduction rule", and it is usually paired with an "elimination rule". Lean calls these eliminators or recursors, although the latter terminology only makes sense for a non-recursive type so it would be a bit of a weird choice if the language doesn't support recursion through this mechanism. So for example the introduction rule for 'and' is A -> B -> A /\ B and the elimination rule is A /\ B -> A and A /\ B -> B. In lean this is exactly the same thing as a constructor and the two projections, so that's why those names get conflated.

Also, as an aside, I do not get where the term 'projection' for dot notation (or destructors) came from -- I suspect math -- but it strikes me as wholly unintuitive jargon.

As for why "projection", the reason comes from the product type, which is a structure with two fields fst : A and snd : B. These functions of types A x B -> A and A x B -> B are called projection functions in mathematics, and the reason for this is because of the geometric effect of the function, for example if you have some shape in R^2 and get the image of the first projection you get its "shadow" on the y-axis. There are other kinds of projection in mathematics like stereographic projection but they all involve some kind of noninjective map and a lowering of dimension.

[Mac]

Mario Carneiro

at the memory level lean's constructor is allocating memory and filling it with provided stuff, so I don't think it is a misnomer at all.

This is an implementation detail, not part of the conceptual abstraction, thus I have qualms with it bleeding into the terminology. Furthermore, during compilation various optimizations can 'constructors' entirely stateless (evaluate them at runtime, turn it into an immediate, etc.). So even a implementation level, this is not necessarily a correct description.

An alternative view point from formal logic is to call this the "introduction rule", and it is usually paired with an "elimination rule". Lean calls these eliminators or recursors

Yep, I personally quite like this terminology, though I realize it also may be unintuitive for some.

As for why "projection", the reason comes from the product type, which is a structure with two fields fst : A and snd : B. These functions of types A x B -> A and A x B -> B are called projection functions in mathematics, and the reason for this is because of the geometric effect of the function, for example if you have some shape in R^2 and get the image of the first projection you get its "shadow" on the y-axis. There are other kinds of projection in mathematics like stereographic projection but they all involve some kind of noninjective map and a lowering of dimension.

Ah, so my suspicious was correct -- math is the culprit! I would say the complexity of that explanation should be reason enough as to why 'projection' is very unintuitive terminology. :upside_down:

[Mario Carneiro]

I won't deny that the word "projection" has travelled far from its roots, but it is still fairly standard CS terminology to call the functions out of a record/tuple type projections

[Mac]

That last point is something of a pet peeve of mine in mathematics. Jargon in math generally takes way to many level of allegory to explain. For example, in this case 'projection' requires about 7 levels of allegory (physical shadow -> geometric projection of a shape -> geometrically reduces dimension -> mathematical projection function -> product type projection -> field projection -> dot notation).

While jargon in computer science also often to involve allegory, it tends to be more direct. For example 'constructor' (physical construction -> abstraction construction). A more technical example could be something like a tail call (tail of an animal -> end of an object -> call at the end of a procedure).

(fyi, I wrote this as continuation to my previous statement, but didn't finish it before you responded XD)

[Mario Carneiro]

googling field projection reminds me also that this is standard terminology in databases - selecting one field from a table is called a projection operator

[Mac]

Well there are a lot of mathematicians in computer science so I would expect the terminology to mix. :laughing:

[Mac]

That doesn't make the terminology any more intuitive to the uninitiated (or those not as mathematically inclined).

[Mario Carneiro]

Mac said:

Mario Carneiro

at the memory level lean's constructor is allocating memory and filling it with provided stuff, so I don't think it is a misnomer at all.

This is an implementation detail, not part of the conceptual abstraction, thus I have qualms with it bleeding into the terminology. Furthermore, during compilation various optimizations can 'constructors' entirely stateless (evaluate them at runtime, turn it into an immediate, etc.). So even a implementation level, this is not necessarily a correct description.

Well you are the one saying it has to be stateful. I think a constructor only needs to construct an element of the new type, and whether that is pure or not is besides the point. I prefer my constructors to be pure functions, even in impure languages.

[Mac]

For me, when my brain hears projection, it thinks of the physical phenomena and is incapable of properly connect that to the abstract concept. Even with that background, the connection is too distant for my brain to internalize it as intuitive.

[Mario Carneiro]

also, your description of compilers playing tricks with constructors applies just as much to new Foo() in java, which are for me the ur-example of constructors in CS

[Mac]

Mario Carneiro said:

Well you are the one saying it has to be stateful. I think a constructor only needs to construct an element of the new type, and whether that is pure or not is besides the point. I prefer my constructors to be pure functions, even in impure languages.

Fair. While I do personally find it pure constructors/destructors a little counterintuitive, I do admit they are still often the best terms for the concept (as I mentioned before).

[Yakov Pechersky]

Yes, language is overloaded, especially in particle physics: spin, flavor, charm...

[Mac]

@Yakov Pechersky Yep. Neologisms and overloaded language are quite a common part of math, philosophy, and computer science. While any new jargon is confusing at some level, it is a necessary part of formalization and I have no problem with it in general. My problem is when the overloaded definition is far removed from its natural definition even when reason for the name is explained.

[Mac]

For me at least, distance connections make it extremely hard to remember the overloaded meaning as my brain keeps trying to default to natural meaning and the clash causes cognitive dissonance.

[Mac]

Mario Carneiro said:

also, your description of compilers playing tricks with constructors applies just as much to new Foo() in java, which are for me the ur-example of constructors in CS

True. For me, though, there is a difference conceptually at where the optimization occurs.

Part of the defined behavior of the constructor new Foo() in Java is to constructor a new Foo in memory. Thus, when optimization is turned off, it will always construct a new Foo in memory. In a pure language, however, It is not part of the defined behavior of a constructor to allocate memory. Thus a compiler, even with optimization turn off, can choose to compile a constructor to something else (e.g., because it is more efficient to do so).

In C++ terms, in an imperative language, memory allocation is part of the standardized behavior of a constructor. In a pure language, it is not. It is instead part of the compiler-specific behavior of the constructor.

[Mac]

This difference in the what is the defined behavior of a constructor is why I consider the application of the same term to both cases to be a (little) bit of a misnomer.

[Mario Carneiro]

That kind of analogy is pretty common in programming languages. Sure it's not exactly the same as the imperative case, but the word constructor doesn't fit any other concept in the language better

[Mario Carneiro]

Here are some common CS jargon words that are quite removed from their original meaning:

block, boot, bug, class, closure, code, daemon, execution, glob, inheritance, linker, stack, subroutine

[Mac]

Mario Carneiro said:

Here are some common CS jargon words that are quite removed from their original meaning:

block, boot, bug, class, closure, code, daemon, execution, glob, inheritance, linker, stack, subroutine

I disagree largely with this list. I would consider 'block, class, code, and execution' to be direct parallels, 'linker, closure, stack, inheritance, subroutine' to be close parallels. I would also consider 'bug' to be a close metaphor and only 'daemon and glob' to be esoteric.

[Mario Carneiro]

close parallel to what? A programming error is not like an insect at all, a code block is not a "cuboid piece of substance" to borrow wiktionary, "execution" is not how you kill people unless you are a malfeasant programmer

[Mario Carneiro]

anyway this is just how language goes. Meanings evolve from other meanings, and if you trace it all back you get some odd results

[Mario Carneiro]

there isn't anything to be said for intuitive naming besides "you get used to it"

[Mac]

@Mario Carneiro The word execution is defined as ""a carrying out, a putting into effect" which is exactly what it means in CS. (its use to describe the death penalty is simply a euphemistic use of this meaning) . Block in CS (i.e. 'a block of text') comes from a 'block of text' where block is used to mean a large chunk/piece of something. The word 'block' initially being used to mean a piece/chunk of wood.

[Mario Carneiro]

I'm aware that in each case there is a chain of meaning, often quite logical

[Mac]

My point is that they are directly related to their natural language meaning and etymology.

[Mac]

With, at most, one level of analogy/metaphor.

[Mario Carneiro]

most math terms have the same kind of chain, but one is limited by the strength of analogy to something abstract

[Mac]

This would be the same for a geometric projection of an image in space. That is one hop. Going from that to a projection is CS is like another 5 hops that require mathematical expertise to see the logic in.

[Mario Carneiro]

I thought of putting "global" on the list, but the meaning of "everywhere" is also common, even though it originally derives from "round"

[Mac]

Mario Carneiro said:

most math terms have the same kind of chain, but one is limited by the strength of analogy to something abstract

Yes, the problem here is the 'chain' part. Jargon should ideally be directly analogous (either by parallel or metaphor) to its natural meaning.

[Mac]

The problem I have with jargon is in math is that that it makes jargon of jargon of jargon (and so on).

[Mac]

Instead of just making different terms (or composite terms) for things.

[Mac]

As a CS person, I do sympathize with the desire, for example, to not call a 'group' a 'unital invertible associative magma'. (we do like our short terms) But I would at least like the term to have a close analogy (even by metaphor) to its definition in natural language.

[Mac]

This is also why I like the term 'binar' better than 'magma'. It at least incorporates the fact the the function in question is binary.

[Mac]

Admittedly, there is often not good analogues to be had for some very abstract concepts and thus largely arbitrary terms are sometimes needed. One of the reasons to teach math to children is so that they can learn these arbitrary terms at the same time the are learning natural language so that the become intuitive words in their vocabulary.

[Mac]

Once a person becomes an adult it is much harder to learn such arbitrary language. This is in part why learning a different (natural) languages as an adult is so hard.

[Steven Obua]

@Mario Carneiro When you send around the request for CICM videos I realised just then that you had a new paper out on CICM, and I checked it out this morning. No wonder that you are the only one I've found so far who is interested in Practical Types! I see that with MM0 you have a very similar approach to theorem proving as I do now. Practical Types and MM0 need to solve similar problems, and it is interesting to look at what the differences are. I have now implemented a first version of a Kernel for Practal Light (that sits in a separate branch currently), with the one missing feature being typedef, which is next in the works. So I see clearer now on a few points. "First-Order Abstract Syntax" seems to be a really useful concept that works very well for me so far. I am not sure if it is new, or if it has been around under other names already. I think what it does is solve the same problem as Higher-Order Abstract Syntax, but not introduce function sorts, etc., but stay first-order. In MM0 you also need to solve the binder problem, and you seem to do that with the V(t) / FV(t) mechanism, and by including the names of dependent variables in the types of meta-variables. In Practal Light, meta variables are just the free variables, and the type of these meta variables is just their arity. I have two term representations now: Term, which doesn't explicitly distinguish between bound and free variables, and Tm, which is based on de Bruijn indices, and much better suited for things like substitutions. I am currently converting between the two in the kernel, but for an efficient implementation I should probably just stick to Tm internally and reserve Term for the frontend.

Implementing the Kernel also cleared up some other issues for me. In particular, it makes a lot of sense to design Practal Light also as a logical framework, just as MM0 is a logical framework also. In the beginning I conceived Practical Types as a whole, but it is better to break it down. You voiced concerns earlier about the underlying logic being too complex and not simple enough, and I think that should address your concern. The kernel doesn't know about most of Practical Types so far, and it should stay that way, except for typedef of course, which is not implemented in the kernel yet. The kernel currently only knows these constants:

• Truth ⊤
• Propositions ℙ
• Equality =
• Type membership :
• Conjunction ∧
• Implication ⟶
• Universal Quantification ∀
• Existential Quantification ∃

Furthermore it has the concept of a context, and lifting theorems between contexts. The typedef feature needs to be added to complete the kernel.

The rest of Practical Types can then be built on top of this Kernel, but so can intuitionistic logic, paraconsistent logic, etc. (at least I believe so, currently). So this is very similar to MM0, but I am pushing EVERYTHING into a uniform universe of logical discourse, including sorts (which are just types introduced via typedef), for example wff in MM0 corresponds to ℙ, the only type built into the kernel. It would be very interesting to know if Practal Light can in principle achieve similar speeds as MM0, or if V(t)/FV(t) is superior for that purpose.

[Mario Carneiro]

Note that what MM0 calls "sorts" are really more like syntactic classes for logical entities than types. In fact they are deliberately too weak to get any kind of interesting type system going in the sorts. Usually, a logical theory will have only a few of them. For example in HOL-in-MM0, the sorts are terms and types; in DTT they are terms, in FOL they are terms and propositions. Metamath + ZFC has a second order thing going on with sets, propositions, and classes. I'm not sure whether types constitute a separate syntactic class in your case so I think in practal they would be either terms or terms and types.

[Mario Carneiro]

I don't think it is inevitable that typedef should be part of the kernel. If you go that route it is sure to be by far the largest part, just as inductive types are in lean. Instead, see if you can axiomatize it so that you don't need complicated definition schemata in the kernel

[Mario Carneiro]

I think your list of built in constants is still larger than it could be, and it also seems to bake in a notion of first order logic, which means that it's not clear how to represent weaker systems. The MM0 kernel doesn't have any constants built in, but it does have a notion of definitional equality similar to (but much weaker than) lean's which is used to implement definitional unfolding. The user can't manipulate this equality relation directly, it's not a binary operator in the logic itself.

By the way, I believe that MM0 would work just as well with V(t) being replaced everywhere by FV(t). I suspect it is slightly less efficient but that is just an untested hypothesis.

[Mario Carneiro]

The primitive rule "introducing a constant from an existence theorem" sounds like the axiom of choice, so that's shutting out the intuitionists. You might not care, but it's good to be upfront about that sort of thing.

[Mario Carneiro]

The rules on contexts sound like the module system I considered and discarded early in MM0's design. The reason I didn't go for it was because I determined that it is possible to simulate such a system without the kernel's assistance, and MM0 is aiming to have the most bare bones kernel that can efficiently support the common high level reasoning patterns in formal mathematics. Practal seems to be aiming more to be the front end itself, rather than the foundation on which the front end is built, so it makes sense that there would be divergence at this point.

[Steven Obua]

You make important points, let me go through them one by one:

• Yes, sorts are very weak types. Isabelle has them too. Practal doesn't have them as separate syntactical entities, because everything is a term. But you can make new sorts via typedef as objects in the universe. In that sense, Practal is simpler and more uniform than MM0!
• Practal's typedef will be much simpler than what you seem to have in mind, I don't think it has much to do with inductive types as in lean. It is more a special kind of definition that can create "bubbles" within the universe that are guaranteed to not overlap with other bubbles. And you are right, it should actually be possible that it just introduces axioms, given that a type is just a constant with some properties! But let's say that you have 100 different bubbles, then you need (100*99/2) axioms to state that they are pairwise disjoint without trying to be clever about it. So these axioms should be generated on the fly. That's why I put typedef automatically into the kernel in my mind, but of course there is no reason why that axiom generation should not just happen outside of the kernel, with a "source" attached to them of where they come from, in that case typedef.
• I guess the question of how many constants a foundation has depends on what you count as constants. MM0 has the sort relationship, that's the constant : in Practal, except that Practal's : is both simpler and more powerful. A logic that doesn't have propositions, truth, implication and conjunction is not that practical, so these are OK as well. Universal and existential quantifiers are necessary because they allow to talk about the universe. That there is a universe to talk about is an assumption built into any logic that can be modelled with Practal, that is right, but also a very practical assumption, because without any universe, what are you talking about?
• Contexts work in a very natural and simple way. I have experimented with them before. In Practal they boil down to their essentials and the cruft of previous designs has been removed from them. Experience will show how much cruft is still left in the current design. I basically don't think a sane implementation of Practal should be done without contexts. Also note that EVERY ITP system needs some sort of notion of context for representing the hypotheses of theorems, and I would not expect MM0 to be an exception in that regard. And yes, it should be easy to implement modules on top of them. In my opinion, that works actually in favour of them, not against them. I believe because of Practal's uniform design it is simpler to provide them in Practal than it would be in MM0. For example, contexts don't need to track sorts, especially with a typedef that is not part of the kernel.
• "Introducing a constant from an existence theorem" might indeed be inviting the axiom of choice in through the backdoor, but that depends a lot on what kind of existence theorems you can prove in your logic. For example, if you have intuitionistic logic, then this should not imply the axiom of choice. If you use classical logic, then it will. I think that is reasonable, but yes, it should definitely be mentioned on the packaging. Right now contexts are baked into the kernel, but maybe it should be possible to introduce types of contexts just like you can introduce axioms and constants.
• Practal aims to provide both a frontend AND a foundation, but the goal of its foundation is not to be minimal or being able to model every logic out there. The goal of its foundation is to be simple and easy to understand, but still to be able to cover the entire reasoning spectrum that a mathematician would expect. The goal is that when a user of Practal wants to understand how it works under the hood, Practal's foundation explains EVERYTHING, in a simple way.

[Steven Obua]

I actually don't think that the choose context implies the axiom of choice. It basically corresponds to the deduction rule
(Γ,φ(x) ⊢ ψ) ⇒ (Γ, ∃ x φ(x) ⊢ ψ) if x is not free in ψ or any formula of Γ
that I copied from "Logic and Structure" by Dirk van Dalen, Lemma 3.9.1 (ii).

[Steven Obua]

Contexts really just correspond 1-1 to natural deduction rules like the rule for existential elimination above, so it is actually hard to imagine having a simpler and more natural implementation without contexts.

[Mario Carneiro]

What plays the role of ψ in your context then?

[Steven Obua]

That is the formula that you prove in the context.

[Mario Carneiro]

Could you sketch how the user would encounter a rule like this in a practal file?

[Steven Obua]

It's not clear yet how the practal file exactly would look like, but it is implemented in the kernel here: https://github.com/practal/practal-light/blob/9146aaf52df1ba3afda8f0708cc2c0d13b528980/Sources/practal-light/Kernel/KernelContext.swift#L224

[Steven Obua]

That describes the lifting of ψ out of a choose context.

[Steven Obua]

But basically it should look like this:

choose `x` such that `φ(x)` (proof obligation: `∃ x. φ(x)`)
....
have  ψ

[Mario Carneiro]

Yes, sorts are very weak types. Isabelle has them too. Practal doesn't have them as separate syntactical entities, because everything is a term. But you can make new sorts via typedef as objects in the universe. In that sense, Practal is simpler and more uniform than MM0!

Those aren't sorts, if they aren't new syntactic classes. So it sounds like you are saying Practal has only one syntactic class of terms, similar to DTT. This is a reasonable choice, although it has consequences elsewhere...

Practal's typedef will be much simpler than what you seem to have in mind, I don't think it has much to do with inductive types as in lean.

I'm talking about the complexity of syntax and semantics needed to specify schemas like this one. Already there we see lots of syntactic classes that aren't terms: lists of identify, constraints, constructors, with/in/where modifiers. You will either need a lot more built in constants, or another syntactic class separate from terms to encode the space of valid typedef specifications. Not to mention all the proof obligations that this kicks up, and how to describe those obligations as well. This is all fairly close to the complexity of an inductive specification, which has a list of constructors with types, and a bunch of constraints / proof obligations on top to ensure positivity and generate the recursor and equations.

[Steven Obua]

But that syntax is just frontend, as you would say. The kernel itself does not contain any of that. This is just like you can have elaborate packages in Isabelle for defining recursive functions, but the Isabelle/HOL kernel just allows for a fixpoint combinator.

[Steven Obua]

Maybe there is a misunderstanding here. When I say that Practal wants to be both frontend and foundation, I don't mean that frontend and foundation are the same. I mean that there is a frontend, and a kernel, and these are separate entities. The kernel provides the foundation, and the frontend the sugar on top of it.

[Steven Obua]

As for sorts / syntactical classes, what I mean that what you are able to achieve with sorts in MM0, you can achieve with types generated via typedef in Practal. These types are not separate syntactical classes, but that is the point.

[Steven Obua]

That means that you can reason about them, while you cannot really reason much about sorts.

[Mario Carneiro]

I guess the question of how many constants a foundation has depends on what you count as constants. MM0 has the sort relationship, that's the constant : in Practal, except that Practal's : is both simpler and more powerful.

A constant is a term or term constructor which the user can use arbitrarily in other terms. Metamath and MM0 take the approach of having no actual constants, with all primitives being expressed at the meta level, so that they don't unduly affect the provability relation. As I understand it, Practal's constants are actually constants in this sense.

A logic that doesn't have propositions, truth, implication and conjunction is not that practical, so these are OK as well. Universal and existential quantifiers are necessary because they allow to talk about the universe. That there is a universe to talk about is an assumption built into any logic that can be modelled with Practal, that is right, but also a very practical assumption, because without any universe, what are you talking about?

You might be studying pure modal logic, where there are no quantifiers, or session types, where implication is linear and quantification is optional, or primitive recursive arithmetic, where there are only bounded quantifiers. Again, it's a choice if you want to consider these weird logics as in scope or not. MM0 made the explicit choice to reject the MIU "logic", at least with the metamath inspired encoding, because of its undesirable constraints on more normal proof systems.

Also note that EVERY ITP system needs some sort of notion of context for representing the hypotheses of theorems, and I would not expect MM0 to be an exception in that regard.

Yes and no. Metamath and MM0 are both based on (tuned for) hilbert-style axiomatizations, which basically means that the proof judgments look like ⊢ φ instead of Γ ⊢ φ. This is tempered by the ability to locally assume that a theorem is provable, but this is more like ⊢ ψ => ⊢ φ than ψ ⊢ φ. The most obvious difference is that in metamath/mm0 there is no hypothesis discharge rule. You can then layer a hypothesis system on top of this if the logic supports it (i.e. there is a -> operator that acts sufficiently like implication). This approach is necessary for directly supporting logics that require control of the context, like modal logic (or first order logic, for that matter, if it's not already baked into the system).

[Mario Carneiro]

Steven Obua said:

But basically it should look like this:

choose `x` such that `φ(x)` (proof obligation: `∃ x. φ(x)`)
....
have  ψ

Is there a sectioning mechanism, or a way to know what the goal is at the point you have the choose line?

[Mario Carneiro]

Steven Obua said:

But that syntax is just frontend, as you would say. The kernel itself does not contain any of that. This is just like you can have elaborate packages in Isabelle for defining recursive functions, but the Isabelle/HOL kernel just allows for a fixpoint combinator.

Right. I'm interested to know what the analogue of the "fixpoint combinator" is for your typedef.

[Mario Carneiro]

Steven Obua said:

That means that you can reason about them, while you cannot really reason much about sorts.

Yes, this is the distinction I'm getting at. A sort is essentially metatheoretic structure that you use to define the theory you want to work in. You can't directly reason about it in the logic because that would be part of the metalogic. Making the logic the same as the metalogic tends to really pump up the consistency strength of the system, and if you are not careful you can make the system inconsistent this way.

[Steven Obua]

Right. I'm interested to know what the analogue of the "fixpoint combinator" is for your typedef.

Me too! I will let you know once it is implemented.

[Mario Carneiro]

The analogue in practal would be something like proving something by induction on terms and typedef constructions

[Steven Obua]

You cannot talk about terms in Practal, or about typedef constructions. You can just use terms, and use the axioms generated by a typedef. Therefore, I don't think there is any danger of a "pump up effect" in Practal. But yes, you have to be very careful in implementing any kernel.

[Steven Obua]

I was initially worried about inconsistency issues in Practical Types, but the more I work with / on them, the less worried I become. It is really just all very straightforward and just simplifies existing systems, for example not needing sorts and having just a single syntactical class of terms, but at the same time not going down that rabbit hole of curry-howard.

[Steven Obua]

As for sectioning, imagine each context starting its own reasoning branch. There is no goal, just a sequence of theorems you prove in some context.

[Steven Obua]

Each theory development will have a main branch of contexts. You can bring theorems proved in contexts that branch of that main branch by lifting them back into the contexts of the main branch.

[Steven Obua]

Basically each context is its own mini-kernel, and without lifting the theorems you prove are only valid in that context, not in any other.

[Mario Carneiro]

Steven Obua said:

As for sectioning, imagine each context starting its own reasoning branch. There is no goal, just a sequence of theorems you prove in some context.

In that case, I don't see how you can make use of the rule "(Γ,φ(x) ⊢ ψ) ⇒ (Γ, ∃ x φ(x) ⊢ ψ) if x is not free in ψ or any formula of Γ" to justify your constant introduction rule. The formula ψ is not determined at the point of the rule, so it must somehow mean "all theorems I am about to prove"; but those theorems can reference the new constant, so "x is not free in ψ" will not be satisfied

[Steven Obua]

It works like that: You enter the context Γ,φ(x) and you start proving theorems. Say you proved a theorem ψ. If ψ does not contain x, then you can lift it out into the context Γ, ∃ x φ(x). That's the deduction rule. If ψ contains x, you cannot lift it out of the context, but just their existential quantification ∃ x. ψ.

[Steven Obua]

This is also the deduction rule, together with the introduction rule for the existential quantifier.

[Steven Obua]

I have an additional rule for existential introduction in the kernel, but I guess I could just drop that, as it is part of how lifting for the choose context works. That part of the lifting code is also much simpler than the code for the additional rule.

[Steven Obua]

Or rather not, I cannot drop it.

[Steven Obua]

But I could drop the part of the lifting code that converts ψ into ∃ x. ψ and just demand that this is done explicitly via existential introduction. I think.

[Steven Obua]

Or actually I think I CAN drop it, as I can always enter the choose context like that:

choose x such that `∃ x. ⊤`
...
have `ψ[x]`

[Steven Obua]

That would require an additional axiom ∃ x. ⊤, though.

[Mario Carneiro]

is that an unbounded quantifier btw, or is there a type somewhere?

[Steven Obua]

Unbounded first-order quantifier.

[Mario Carneiro]

it ranges over all objects, types, everything?

[Steven Obua]

Yes.

[Mario Carneiro]

that seems kind of inconvenient for normal uses of choose

[Steven Obua]

Why? You can just use the bounded version ∃ x: S. φ which is defined in terms of ∃

[Mario Carneiro]

I think it would be good for you to mock up what a user's interaction with the system would look like, including all the file level / module level stuff. My first public discussion of MM0 was accompanied by a file that defined the axioms of ZFC and proved some trivial things, or at least purported to do so since the parser hadn't been written yet at the time

[Mario Carneiro]

it makes it easy to discuss things like concrete syntax, as well as motivate the role that each rule and bit of syntax has in the system

[Steven Obua]

That definitely needs to happen at some point, as it constitutes the frontend, but I have done that before so I know already how that will work. So I am currently just focusing on getting the foundation right, but having that piece of frontend would make it definitely simpler in discussing it with somebody!

[Mario Carneiro]

You might find out that some part of your design doesn't work well once you have the mockup. That happened to me with MM0, it turned out that the syntax I had chosen for delimiting math sections was hard to read and I changed it based on feedback

[Steven Obua]

Sure, that will definitely happen, but I consider that just as normal iteration of software. I was more worried about doing something hilariously inconsistent, but I know now that it will work :-) This discussion was already very valuable to me!

[Steven Obua]

From a pure frontend point of view, you cannot go much wrong by just following the looks of Isabelle/Isar. It just all becomes so much more simple and powerful, because of the uniformity of Practal's foundations.

[Steven Obua]

The basic looks will be similar as here in ProofScript, which also uses contexts:

• https://github.com/proofpeer/proofpeer-proofscript/blob/master/scripts/root.thy
• https://github.com/proofpeer/proofpeer-proofscript/blob/master/scripts/bootstrap/classical.thy

The basic logic in ProofScript was set theory embedded in higher-order logic though, and that's just not good enough.

[Steven Obua]

Also, the focus of ProofScript was wrong. I tried to make a programming language perfectly designed for scripting proofs, but that's not what is needed. I call it the "bootstrap trap". What is actually needed I wrote down in the Practal position paper.

[Mario Carneiro]

there aren't any proofs in the code examples there though

[Steven Obua]

There are proofs in the second file?

[Steven Obua]

Everything that comes indented after a theorem is a proof.

[Mario Carneiro]

I mean in the practal position paper

[Steven Obua]

Ah :grinning_face_with_smiling_eyes:
Well, a proof really should be just a sequence of theorems, the intermediate steps being filled out by automation. Very similar to what an Isabelle/Isar proof looks like. So contexts in Practal then basically correspond to contexts in Isabelle/Isar. It's pretty clear how that is supposed to work, so I have not given it any attention in the paper.

[Steven Obua]

I've roamed the internet in search of support that the "choose" context is fine, and here is what I found:

Before proceeding to the next stage, let us clear up one last misconception. Suppose that in a mathematical text we have the assumption that there exists x such that φ(x). We customarily say “choose an x satisfying φ(x)” to give ourselves an x satisfying φ. This is not an application of the axiom of choice, but rather an elimination of an existential quantifier. Similarly, if we know that a set A is inhabited and we say “choose x ∈ A”, it is not choice but existential quantifier elimination again.

This is a quote from "Five stages of accepting constructive mathematics" by Andrej Bauer, at the end of the first section "Denial".

[Steven Obua]

So this matches my initial intuition: Given an existence theorem, choosing an x such that it has the corresponding property is fine. Because what would existence mean otherwise? This is just existential elimination. The axiom of choice is not about existential elimination, but about which objects you can prove to exist in the first place.

[Mario Carneiro]

I'm aware of the rule of existential elimination, but it is dubious to apply it at the top level, when you aren't proving any particular theorem. There is a choose like tactic in lean (actually called cases) for unpacking an existential, but it only works inside a proof, so there is a current goal, and it has restrictions on the goals to which it will apply, which you can't possibly check if you don't know what the goal is

[Steven Obua]

On the Kernel level there is no such thing as a proof in Practal, just various ways for constructing theorems. Of course you can call such a construction a "proof", if you want. There is not really such a thing as a "toplevel" as well, each context forms its own little world in which you create theorems. A context can have a parent though, and you can form chains of contexts in this way, and there are rules for how to move a theorem between contexts along such a chain. Note that Bauer doesn't mention anything about toplevel or tactics, either... So I am pretty sure there is nothing dubious about it.

[Mario Carneiro]

Do you have a formal (abstract) syntax for the language? What are the syntactic elements in the file, and what are their meanings? This is a major question that the practal paper does not address. Looking at the linked bit of code, I see assume, choose, declare, define, seal, and none of these are discussed in the practal paper

[Mario Carneiro]

For a language like yours, a "proof" is the syntax that is translated into kernel calls to construct theorems, so the structure / extent of this syntax is very important for users

[Mario Carneiro]

and that's not even talking about concrete syntax, i.e. where you put the punctuation, just the actual moves available to the user

[Steven Obua]

I absolutely agree with you, syntax is very important. That's why I developed a new semantics for parsing in terms of pyramid grammars. This will make user-extensible and composable syntax possible for Practal.

The Practal position paper presents a vision of what an ITP system should look like. So of course it doesn't contain all details worked out. I am right now working them out! Practal doesn't exist yet, but it is progressing much faster currently than I was expecting when writing that paper. Turns out, once you have defined for yourself clearly what you are going after it becomes much easier to achieve it! The practical types stuff I created just shortly after setting out that vision. A first version of the kernel is already finished apart from defining and implementing typedef. Within one or two months (I wish earlier, but I need to work on other things as well so I can eat), expect another paper / another iteration of the practical types paper that explains contexts, assume, etc. You can also look at my ProofScript paper, contexts work a lot like described there, but it is cleaner and nicer now.

If you want to know what the syntax will look like, you can just look at Isabelle/Isar and the Archive of Formal Proofs, or at the ProofScript code I linked. It will look a lot like that. Given that it is all converted into Kernel calls, one can iterate quickly on what it exactly looks like depending on what works best. Finding the best concrete syntax will be an iterative process. It's not something you start with set in stone. Exactly because it is so important for the user, as you rightly pointed out.

[Mario Carneiro]

I'm trying to say that the focus is not the concrete syntax, but rather the abstract syntax, and what you call kernel calls. Suppose the user didn't have any syntax apart from calling the kernel directly; what would those trees of kernel calls look like? When are they accepted / rejected, what are the side conditions and so on

[Steven Obua]

It's all in the code. If you call the kernel and it gives you back a theorem, then this theorem is valid in that context. You could start proving right now, but it will not be pretty as it will be just Swift code, and there is no automation yet apart from First-Order Abstract syntax pattern matching.

[Mario Carneiro]

Pointing to AFP is not very helpful for understanding what your system will do because isabelle is huge and you will not implement it all (and there is probably a fair amount you don't want to implement even given infinite time). That's a way to indicate the general style of the concrete syntax, which is fair enough, but again, concrete syntax isn't so important because it is easy to change

[Mario Carneiro]

So you have a novel proof theory which has no specification apart from the code?

[Mario Carneiro]

I mean, you wouldn't be the first to do so, but it's not a good idea

[Steven Obua]

No, it is the part of the specification that is available right now. The practical types paper is another one. The practal position paper is another one. If you want ALL the details and not piece them together yourself, you will need to wait. Or pay me about £20000, and you will get them in two or three weeks :-)

[Mario Carneiro]

I'm mostly trying to understand roughly how the system is laid out at a logical level. Is there an actual paper BTW, or are you talking about the two HTML pages?

[Mario Carneiro]

My main argument is that it is good to have such information available for yourself upfront, so that you can avoid backing yourself into a corner with a feature that leads to contradiction

[Mario Carneiro]

Once you have a sketch of the argument for how deductions in the kernel map to something in FOL as traditionally conceived, you will find it much easier to justify and add more proof rules to the kernel

[Steven Obua]

You can print out the two HTML pages, they are about paper size :-)

As I said, for information about contexts, you could look at the ProofScript paper. It is an actual paper, but I would say that the two HTML pages are more important.

I have a sketch of how deductions map. It is really just first-order logic. And contexts make it rigorous of what proving actually means, just like sequent calculus etc., but better, because, 2021 and computers. For example, the choose context is just existential elimination, as we discussed. You are probably not familiar with Isabelle/Isar and in particular Isar contexts, otherwise how the system is supposed to work would be clearer to you, I think.

[Mario Carneiro]

Isabelle has a bunch of other stuff like locales though and I'm not sure what you are doing at that level

[Steven Obua]

Locales come basically for free with contexts. At least that's what I believe right now, as I have not worked through that yet. At lot of work in getting locales right consists in dealing with type variables, etc., and in general getting locale stuff converted into Isabelle kernel stuff. That should not be a problem in Practal, as the kernel is designed from the start supporting contexts.

[Mario Carneiro]

I see here that you are universally quantifying any assumptions that have been made. I assume that is because you have a mechanism to instantiate a hypothesis. But then how do you prove x > 0 -> x > 0 and not (\all x, x > 0) -> x > 0?

[Steven Obua]

Yes, because free variables are implicitly universally quantified; so if they are contained in an assumption, they need to be explicitly quantified over. I find this a little bit confusing, and in the beginning I was just forbidding free variables in assumptions. But then I started to write down a few axioms, and being able to use free variables was just very practical. So I allow it now. In the frontend there needs to be a clear visual distinction between free variables and constants, then it will not be confusing, I think.

The way to prove x > 0 ⟶ x > 0 would be like that:

context
  declare x
  H: assume x > 0

print H

So you would first introduce the constant x. Then make the assumption on x.

When the theorem is printed, is has been lifted out of the context in which it was originally stated into the context where it is printed, and it will have the form x > 0 ⟶ x > 0 where x is a free variable now.

By the way, I just reread the Practal position paper, and some things are already outdated by now. For example I still think there of ∀ having a dependent type, which is not the case anymore. Sorry for that! I hope this all stabilizes soon enough and proper documentation becomes available.

[Mario Carneiro]

From your indentation (?) it seems like that would also discharge the declare x, in which case the proof would be showing ∀ x, ∃ x, (x > 0 ⟶ x > 0), if I understand your discharge rules correctly

[Mario Carneiro]

By the way, short examples like that are good. Do more of that (here or in the public docs)

[Yakov Pechersky]

Is there name hygiene?

[Steven Obua]

@Yakov Pechersky Not sure what you mean, so let me guess. Can the declared x in the above example clash with a previously declared x? No, it cannot, each constant you introduce must be different from all other constants declared so far. But there are namespaces, so this is not a real restriction.

[Steven Obua]

@Mario Carneiro The context chain will look like that

Top::
C1:: declare x
C2:: assume x > 0
H

So the theorem H (x > 0) is originally an axiom in context C2. Lifting it into C1 results in x > 0 ⟶ x > 0 where x is a constant. Lifting it further into context Top will turn the constant x into a free variable x.

[Steven Obua]

@Mario Carneiro I've worked more on the foundations of Practical Types. It is not exactly first-order logic, but something I call Abstraction Logic. I've published a report about it: https://doi.org/10.47757/abstraction.logic.1