Re: [HoTT] Re: Where is the problem with initiality?

[Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>]

On 06/06/2018, 00:12, "homotopyt...@googlegroups.com on behalf of
Richard Williamson" <homotopyt...@googlegroups.com on behalf of
rwilli...@gmail.com> wrote:

>Alexander is getting a fair bit of stick! I just wanted to add a
>note of support to one aspect of the point I think he is making:
>there is a reason that languages such as Python are widely used
>by perfectly competent programmers who fully understand the
>benefits of typing.

Actually I am teaching Python (by choice) hence I agree to a point.
However, first of all we can express "untyped" constructions in a typed
setting (e.g. an untyped object is a pair of a type code and an element of
the corresponding type). And second the untyped version is only the first
step before I understand what I am doing at which point I am able to make
the concepts involved more precise. In particular in a mathematical
development I would expect that the objects involved are understood and
hence can be given a specific type.

>
>I share the view that there has to be something rather more
>Python-like in syntax than the currently available syntaxes if
>one is to have any hope of having something usable in practise by
>people who just want to get on with the mathematics. I am not
>convinced that this is a purely engineering problem as opposed to
>a theoretical one.
>
>(Yes, Python is not untyped either, but I think the point
>stands).

Actually, Python is dynamically typed, which is why I always compare it to
set theory. Python has predicates to test wether an object belongs to an
arbitrary type. This corresponds to the element relation in set theory. In
contrast, strongly typed languages don't have predicates like this because
you know statically what the type of an object is. In the same way in Type
Theory typing is static hence it doesn't make sense to have an element
relation.

I would think that once I understand the concepts involved in my
construction I should be able to assign static types to them. That is
certainly the case in programming but even more so for mathematical
constructions. 


>
>On Tue, Jun 05, 2018 at 09:52:26AM +0200, Andrej Bauer wrote:
>> Dear Alexander,
>>
>>
>> On Wed, May 30, 2018 at 12:53 PM, Alexander Kurz <axh...@gmail.com>
>>wrote:
>> >
>> > It is crucial that informal mathematics is untyped. The untypedness
>>is what makes it flexible enough for practical purposes. Formalising
>>mathematics in a proof assistant is hard work. And to a large extent
>>this is due to the fact that everything has to be typed.
>> >
>> > If we ever want to get mathematicians to use proof assistants as
>>casually as they use latex, the problem of untyped vs typed mathematics
>>needs to be solved.
>>
>> I think you made there a coiple of intellectual jumps. In order for
>> your statements to have some weight, you need to consider the
>> following questions:
>>
>> (a) What if formalization of mathematics in existing proof assistants
>> is hard for some reason other than typedness?
>>
>> (b) Most proof assistants that have a large user base are typed. Is
>> this is a big conspiracy on part of the designers, or could it be
>> understood as evidence that typed proof assistants have a certain
>> advantage over the untyped ones?
>>
>> (c) You offer LaTeX as an example of good design. I beg to differ.
>>
>> (d) Informal mathematics is very obviously typed, as witnessed by the
>> fact that authors are always carefully explain the types of various
>> symbols they use (or rely on the culturally accepted notations).
>>
>> The Buffon needle example presents absolutely no obstacle to typing.
>> Perhaps you are mixing up *informal* nature of human mathematics with
>> untypedness? Formalizing Buffon's needle requires a great amount of
>> precision (what is a curve? what does it mean to "throw a needle"? how
>> do we cuunt crossings when there are infinitely many?) which is
>> unavoidable so long as we subbscribe to the mathematical method.
>> Typedness has nothing to do with this fact.
>>
>> With kind regards,
>>
>> Andrej
>>
>> --
>> You received this message because you are subscribed to the Google
>>Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send
>>an email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>
>-- 
>You received this message because you are subscribed to the Google Groups
>"Homotopy Type Theory" group.
>To unsubscribe from this group and stop receiving emails from it, send an
>email to HomotopyTypeThe...@googlegroups.com.
>For more options, visit https://groups.google.com/d/optout.




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.