linkfix
Floris van Doorn
]]>Lean is presented in part of the ICM talk
added these pointers:
]]>Small change to previous edit
Anonymous
]]>Added the Liquid Tensor Experiment as another notable example of math formalized in Lean. Added a link to the Lean community/Mathlib to the references.
Anonymous
]]>fix dead link
Anonymous
]]>Good day! I know this is somewhat off topic but I was wondering if you knew where I could locate a captcha plugin for my comment form? I’m using the same blog platform as yours and I’m having difficulty finding one? Thanks a lot! https://androtestopropills.com/
]]>Why didn’t they follow the convention?
I never completely understood; you’ll have to ask them. It’s true that this is somewhat about the use of the technology rather than the technology itself, but as a practical matter a programming language is hard to separate from its standard libraries, and it could be that they were pushed towards this choice by (mis)features of Lean itself.
Coq’s “Foo is not equal to Foo” errors show that Coq’s pretty printing is ambiguous. This seems extremely Coq-specific, and they probably ought to fix it.
I think Coq has gotten better about this in recent releases. I used to get a lot of “Foo is not equal to Foo” errors that boiled down to universe mismatches, and now it seems that Coq detects when the problem is a universe mismatch and automatically displays the universe parameters in such a case without my having to turn on Set Printing Universes
.
Re #43, I figured identity “types” would just be dynamically testing identity. I’m trying to get at what Richard expects from dependent types beyond refinement types. Decidable (actually, testable) equality types are available with dynamic refinement types.
]]>Re #14:
Criticism #8 (“Structure depends on notation”) is something that’s always rankled me about Lean. I literally couldn’t believe it when I first heard that they’d actually copy-and-pasted the library about “additive monoids” into a library about “multiplicative monoids”. It reminded me of some old arguments with Arnold Neumaier on the n-Cafe .
There’s definitely something wrong if they’re compelled to copy the library for groups just to change the name of the operator. But I don’t see how this could be the fault of the technologies implemented, rather than a stupid misuse of them. In some shallow sense, a mathematical development inevitably depends on the notation: it needs to refer to things somehow. But it’s a strong convention to regard the name choice as meaningless, so that a copy using a different name is “obviously” redundant. Why didn’t they follow the convention?
]]>Wouldn’t you need some sort of Identity type to encode the notion of abelian groups in python? Is a better question not “How to implement inductive families”?
]]>Re #17:
If it walks like an abelian group and quacks like an abelian group, it might just as well be an abelian group!
Richard, what’s your idea of an abelian group in a dynamically typed language? In particular, what happens to the carrier? This is not a wise guy question; module systems (support for structured types) and dependent type systems are closely related. Based on your answer, I might be able to recommend something.
]]>I think dependent types in Haskell will need to happen before python developers even hear about it. Supposedly it will be finished be next year…
]]>Yes. Type checking happens at run time.
]]>I wouldn’t describe duck typing as a buzz word, it is a standard term that I think accurately conveys what is happening. But ’dynamic typing’ would be an alternative. I think #26 gives an indication of how it could look in practise for inductive types. I have no idea how to build an entire theory around it. :-) It may not be a type theoretic question as much, more of a programming language design one.
Re #37: if I understand what you have in mind, I think dynamic typing would handle this as well as static typing, just in a different way. Python today handles subclasses just fine, for example :-).
]]>@Richard #17
If it walks like an abelian group and quacks like an abelian group, it might just as well be an abelian group!
But a ring walks like an abelian group and quacks like one: but sometimes one really wants the ring, and sometimes really wants the underlying additive group. For more richly structured objects (like a perfectoid ring, for instance), it acts like many things, and one has to be precise which structure is being used at any one time. (Not to hijack the thread, but I feel this is a failing in Mochizuki’s writeup of IUTT: he uses all sorts of idiosyncratic mental crutches instead of making the various forgetful functors in play explicit.)
]]>Regarding “duck typing”, I don’t like that term. I’m pretty sure it’s a buzzword that’s not actually meaningful. The gist is that it’s some kind of type system that doesn’t make pedantic distinctions. But you do actually need to eventually say what type compatibility is, and there’s this whole rich “type theory” that studies this, and doesn’t ever talk about ducks. :)
So for example, I have no idea what “duck dependent typing” is imagined to be.
]]>Re #22:
In response to atmacen’s comment about the ugly projection chains, I think it issue is that hiding these in the notation is not always enough unless there is some kind of definitional coherence rule which allows two versions of the “same” projection chain to be treated as the same.
Maybe that’s the “no diamonds” restriction from Hales’ criticism #9. But even with diamonds, in that case Lean should show some projections, so it isn’t ambiguous, but that doesn’t mean it looks as bad as no sugar.
For the rest of your response to me, it sounds like you’re extrapolating from Hales’ criticisms to your own, much tougher problems that Lean happens to not solve.
Coq’s “Foo is not equal to Foo” errors show that Coq’s pretty printing is ambiguous. This seems extremely Coq-specific, and they probably ought to fix it.
]]>Re #22:
in the context of type theory, Nuprl would be a good example of a system which inherits this characteristic of set theory. [breaking abstractions]
Could you give an example of what you mean?
]]>Hehe, I’m just sketching quickly something in the hope that it might intrigue one or two of the type theorists reading, and be a slight help in encouraging this to be taken more seriously. It’s not something I have time for at the moment to properly try to think about, I’m happy to stop here.
(It doesn’t really matter, but in case it reassures someone, Python is one of the languages I use professionally; the differences with today’s Python are deliberate :-)).
I should say, though, that the double
method does compile in today’s Python and will work perfectly well if n is an object which has an add
method, and this is precisely my point. We should not need a whole different paradigm, we should be able to build on ones that already work well.
Take just plain functional languages for instance like Haskell. Nobody I’ve heard of writes REST APIs in Haskell, but Haskell has had an enormously positive influence on languages in which REST APIs are written. Monads for instance have been incorporated in Java (without calling them such) in a way which makes sense (for example the Optional and Stream types) for Java, one has first class functions in Java since Java 8, etc. I think something similar is what eventually needs to happen with dependent types, and indeed my guess is that either it will one day happen, or else dependent types will never catch on in mainstream programming languages in their present incarnation and will be replaced in the end by something else.
]]>Re #29, OK, thanks for taking a look. Maybe this is why I consider that doing what I have in mind would be revolutionary :-).
It is not supposed to compile in Python today, of course. The point is to illustrate how duck typing might work in a setting where we have dependent types (see especially the double
method). If it is use of things like 0 : self
that is bothering you, which of course is not the way one instantiates a class today, that is very deliberate, I think it is clear that the ordinary object oriented paradigm has to be expanded. One could still mix and match with today’s syntax. E.g. one might have
class ConstantList:
def __init__(self, x):
empty : self
append : self -> self
self.x = x
Here the self.x = x
is today’s syntax, the other two lines are the new syntax that allows for dependent (or at least inductive) typing. If one removes those two lines, this will compile in today’s Python and is the correct way to do it.