[gmane.comp.science.types.announce] [Agda] CFP: Dependently Typed Programming (FI Special Issue)

[Jesse Alama]

This may be somewhat inappropriate for mizar-forum, but it seems
noteworthy to me that in the non-exhaustive list of systems for
dependent types mentioned in this recent post to the TYPES forum, mizar
is not mentioned.  Would it be appropriate to write an article on
mizar's dependent types for the upcoming special issue of Fundamenta
Informaticae?  One initial question to consider: does mizar's type
system differ in any interesting way from the type sytems mentioned
below?

Jesse


[ The Types Forum (announcements only),
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hi,

Tarmo and I are editing a special issue on dependently typed  
programming and would be peased to see submissions from people on TYPES.

It would help with our planning if you could let us know in advance  
whether you plan to submit a paper (let's say end by end of July).

Cheers,
Thorsten



                           Call for Papers:

               Special Issue of Fundamenta Informaticae
                      (http://fi.mimuw.edu.pl/)
                    Dependently Typed Programming
         (http://sneezy.cs.nott.ac.uk/darcs/DTP08/journal.html)

                               Editors:
                   Thorsten Altenkirch (Nottingham)
                       Tarmo Uustalu (Tallinn)

Dependently typed programming is using the power of dependent types to
capture relationships between data, internalising invariants necessary
for appropriate computation. When data describe types, we can express
patterns of programming in code. To capture this potential a number of
languages have been proposed and implemented which incorporate some
aspects of dependent types, e.g. Agda, ATS, Cayenne, Coq's CIC,
Concoqtion, DML, Delphin, ELF, Epigram, Omega, OpTT, Pie, PiSigma,  
Ynot for
a non-exhaustive list.

Within the European TYPES project we have organized two workshops to
discuss aspects of dependently programming:

- EffTT, Workshop on Effects and Type Theory
  http://cs.ioc.ee/efftt/
  Tallinn, Estonia, December 2007

- DTP08, Dependently Typed Programming 2008
  http://sneezy.cs.nott.ac.uk/darcs/DTP08/
  Nottingham, UK, February 2008

The special issue is motivated by the desire to give people who have
presented their ideas at those workshops the opportunity to publish
papers on their work. However, we would like to invite everybody
working in this area to submit papers to the special issue. For a more
complete list of topics, please consult the workshop pages following
the links above.

The paper should follow the usual standards of journal papers, and
should be submitted by email (preferable pdf) to one of the editors
before 1 October 2008. We expect that the papers don't exceed 20 pages
(see the FI webpage for style files). We hope to be able to stick to
the following schedule:

        Deadline for submissions: 1 October 08
        Notification of acceptance: 15 January 2009
        Final versions due: 15 March 2009

This message has been checked for viruses but the contents of an  
attachment
may still contain software viruses, which could damage your computer  
system:
you are advised to perform your own checks. Email communications with  
the
University of Nottingham may be monitored as permitted by UK  
legislation.

_______________________________________________
Agda mailing list
Agda-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@...
https://lists.chalmers.se/mailman/listinfo/agda

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.





--
Jesse Alama (alama@...)

[Josef Urban]

Hi Jesse,

> This may be somewhat inappropriate for mizar-forum, but it seems
> noteworthy to me that in the non-exhaustive list of systems for
> dependent types mentioned in this recent post to the TYPES forum, mizar
> is not mentioned.  Would it be appropriate to write an article on
> mizar's dependent types for the upcoming special issue of Fundamenta
> Informaticae?  One initial question to consider: does mizar's type
> system differ in any interesting way from the type sytems mentioned
> below?

I think the reason why the Mizar type system is not mentioned is that
people know very little about it. And it seems to me that there is
practically no research being done on Mizar type system, even though it is
a very "practical" and notrivial thing to have good "type" automation over
set theory. And yes, Mizar's type system significantly differs from
others. So I think it is a very good idea to do more research and publish
about it.

Josef

[Piotr Rudnicki]

All,

At the risk of sounding as a complete ignoramus:

        Why do people bother with various type theories when set theory is
        available?  What is the expected gain?

I have been asking this question for years and never got a convincing answer.


Cheers, PR


On Wed, Jul 02, 2008 at 10:37:42PM +0200, Josef Urban wrote:

>
> Hi Jesse,
>
> >This may be somewhat inappropriate for mizar-forum, but it seems
> >noteworthy to me that in the non-exhaustive list of systems for
> >dependent types mentioned in this recent post to the TYPES forum, mizar
> >is not mentioned.  Would it be appropriate to write an article on
> >mizar's dependent types for the upcoming special issue of Fundamenta
> >Informaticae?  One initial question to consider: does mizar's type
> >system differ in any interesting way from the type sytems mentioned
> >below?
>
> I think the reason why the Mizar type system is not mentioned is that
> people know very little about it. And it seems to me that there is
> practically no research being done on Mizar type system, even though it is
> a very "practical" and notrivial thing to have good "type" automation over
> set theory. And yes, Mizar's type system significantly differs from
> others. So I think it is a very good idea to do more research and publish
> about it.
>
> Josef

--
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr

[Robert Boyer]

> Why do people bother with various type theories when
> set theory is available?  What is the expected gain?

I am weak in history, but I think that the
Whitehead-Russell type theory of Principia Mathematica
was invented to support the formal development of some
of mathematics with a reduced risk of hitting another
paradox, like Russell's paradox, which might prove that
the chosen set theory was inconsistent.  I think one
set theory of Quine was proved inconsistent.

The type theories of folks like Martin Lof, de Bruijn,
and Gerard Huet are even constructive.  Huet does not
like the first order theorem:

    For some x, P(x) or not P(x).

('Why is there something rather than nothing?'
Heidegger once asked.)

Paul Lorenzen did not like the theorem:

    not not p -> p

So some type theories permit one to do lots of very
constructive mathematics without depending upon a
possibly inconsistent set theory, or even on a possibly
dubious first order logic, whose semantics are
generally based on set theory.

Primitive recursive arithmetic (PRA), and the reverse
mathematics program, is another way to get by with
less.  Small is beautiful, you know, at least to some.
Others say size matters.  PRA goes back to Skolem's
idea for avoiding the inconsistencies of set theory by
avoiding quantification over infinite domains.

Frege once remarked something like, 'What is all this
concern with consistency?  Just because it is
consistent that God exists and that He is good does not
mean that a Good God Exists.'  I'm not sure yet what I
would have replied to him.

Bob

P. S. Corrections by any real masters of the subject
out there most solicited.  As Socrates says, the best
sort of thing that can happen to you is to find out
that you're wrong about something!

[trybulec]

Dear Bob,

I do not consider myself a real master of the subject, still I would
like make some remarks.

Robert Boyer wrote:

>possibly inconsistent set theory, or even on a possibly
>dubious first order logic, whose semantics are
>generally based on set theory.
>
>  
>
Why you think that first order logic is dubious (PRA is a first order
theory, isn't it?).

At least we know that first order logic is consistent.
It is true that the proof of consistency may be based on set theory
(just consider  formulae valid in one element model) but one can do
without set theory. Just add to the theory a constant X and an axiom
       for x holds x = X
then eliminate quantifiers and the whole problem is reduced to the
propositional calculus.

Actually I do not know what 'semantics` means, if it is not based on set
theory.

All the best,
Andrzej

[Robert Boyer]

Hi Andrzej,

So good to hear from you.

> Why you think that first order logic is dubious (PRA
> is a first order theory, isn't it?).

I am not sure whether I think that first order logic is
dubious, and I apologize for apparently making you
think that.  I was merely reflecting on the mental
states of some possible people in some possible
universes.

It is certainly the case that Primitive Recursive
Arithmetic can be cast within first order logic, to
resemble, a first-order theory.

However, PRA can also be cast quite independently in a
considerably weaker logical setting.  I think that
officially, PRA is often viewed as a quantifier free
system of equations, implicitly universally quantified
on the far outside.  Good enough for calculation, and
all other government work :).  The induction principle
is cast as a rule of inference: if you can prove the
base case and the induction step, then you may infer a
new theorem by induction.  The definition principle of
PRA gets one all the primitive recursive functions.
Goodstein's book has a nice development of Skolem's
vision, which I think is not dissimilar to McCarthy's
systems for reasoning about Lisp functions, using
cons/car/cdr instead of 0 and s(x).  In official PRA
you cannot even state, much less prove, that theorem of
first order logic I previoulsy mentioned:

   For some x, P(x) or not P(x).

I think that intuitionists and constructivists tend to
regard Primitive Recursive Arithmetic as 'OK', or even
'trivially OK'.  Thus, while they may generally not
accept

       P or not P

for arbitrary P, they will agree that

       for all nonnegative integers x,
         fn(x) = 0 or fn(x) /= 0,

where fn is a specific function, say 'factorial' (!),
that we have defined by primitive recursion.

There is no doubt that one can prove the consistency of
first order logic!  But assuming what?  Nihilo ex
nihilo.  I believe that if you look hard, you can
always find some rational, thinking,
mathematician/logician who refuses to assume whatever
it is you wish to assume to prove the consistency of
first order logic.

To prove the consistency of first order logic, you'd
probably want the notion of a model, a set theoretic
structure.  But in what set theory?  You might need
something, gasp, as strong as Koenig's lemma!  And you
might find someone who is uneasy about assuming that.

I think that instead of contemplating logics, which
always feel a tad artificial to me, one can cut to
heart of the matter by look at 'the thing':

   P(N) =  {x : x is a subset of N}

where N is the set of nonnegative integers.  I mean the
'power set' of N.  Some people won't let you get past
your wish to believe that P(N) exists, or can be talked
about, or treated as more than a string of charcters.
de Bruijn likes to say that mathematical objects have
the same reality as the characters in, say, a Sherlock
Holmes story.

I do not happen to agree 100% with any of the
constructivists and the intutionists.  First of all, I
am too slow and dumb even to say I even fully
comprehend any of their positions.  But I do not assert
that any of them are wrong.  There are too many of
them, and they are all smarter than me, as are you!

But I am also not an agnostic anarchist.  I think I am
sure about the associativity of addition on the
nonnegative integers.  At least up to a Gogol, 10^100,
because we have recently checked that result with 'bdd'
technology, a kind of mechanical propositional calculus
reasoning commonly used in hardware verification. :)

Bob

[Freek Wiedijk]

Jesse:

>This may be somewhat inappropriate for mizar-forum, but it seems
>noteworthy to me that in the non-exhaustive list of systems for
>dependent types mentioned in this recent post to the TYPES forum, mizar
>is not mentioned.  Would it be appropriate to write an article on
>mizar's dependent types for the upcoming special issue of Fundamenta
>Informaticae?  One initial question to consider: does mizar's type
>system differ in any interesting way from the type sytems mentioned
>below?

The answer to your last question is undoubtedly "yes!"

Note however that this is about depedently typed
_programming,_ while the Mizar language is not a programming
language at all.  At least, there is no execution model
for Mizar expressions that I am aware of.

Freek

[Freek Wiedijk]

Piotr,

>At the risk of sounding as a complete ignoramus:
>
> Why do people bother with various type theories
> when set theory is available?  What is the expected
> gain?

I guess the answer is that it's more philosophically
attractive to them.  It's "the right way to construct
mathematics".  Or something like that.

Also, it's much closer to functional programming.  Maybe
they like functional programming?  In type theory you can
"execute" your mathematics like a program, which some people
seem to like.

Of course Mizar also has a type system, so the gain of
having _types_ should be clear to everyone.

However, having a type system and basing your mathematics on
type theory is not the same thing.  (Even the foundations
of HOL, which also consist of typed lambda calculus, does
not count as "type theory" I think.)

There is a very nice paper by Peter Aczel called "On
relating type theories and set theories", which shows how
both worlds correspond to each other.  So maybe in the end
it's the same thing :-)

Although of course _classical_ set theory does not correspond
to _intuitionistic_ type theories.  So I'd like to pose my
own version of your question here:

        Why do people bother with intuitionistic mathematics
        when classical mathematics is available?  What is
        the expected gain?

:-)

Freek

[Freek Wiedijk]

Bob:

>The type theories of folks like Martin Lof, de Bruijn,
>and Gerard Huet are even constructive.

FWIW: de Bruijn's system is not a type theory.  It's closer
to the logical framework "LF".  In such a system you
don't have _any_ foundations (constructive or classical)
from the start.  Instead you start by defining your logic
("axiomatically"), and only then start working on your
mathematics.  De Bruijn himself compares it to a restaurant,
where you can order different kinds of food.  I think.

Henk Barendregt once had a nice analogy, that unfortunately
I don't remember the details.  In it type theory was
intuitionism, set theory was Platonism, and de Bruijn-style
logical frameworks were formalism.  Or something like that.

Freek

[Freek Wiedijk]

Andrzej:

>Why you think that first order logic is dubious

One might say that the intuitionists think that classical
first order logic is dubious :-)  However, that is not the
right way to look at it: classical first order logic is a
subsystem of constructive first order logic (the subsystem
consisting of the negative statements, i.e., the statements
that are equivalent to formulas of the form "not A[]".)

>(PRA is a first order theory, isn't it?).

That is true, but I still experience PRA in the style of
nqthm/ACL2 as weaker than first order logic, as in those
systems you don't seem to have first class existential
quantifiers.

>Actually I do not know what 'semantics` means, if it is
>not based on set theory.

Neither do I, but I'm certain that the term is used by
type theorists, and that in that case they _don't_ consider
themselves to be doing set theory.  (I guess that when they
talk about semantics they "just" interpret one theory in
another one.)

Freek

[Freek Wiedijk]

Bob:

>But I do not assert that any of them are wrong.

As Pauli said it: maybe they're not even wrong :-)

Freek

[trybulec]

Freek Wiedijk wrote:

<>Andrzej:

One might say that the intuitionists think that classical
first order logic is dubious :-) However, that is not the
right way to look at it: classical first order logic is a
subsystem of constructive first order logic (the subsystem
consisting of the negative statements, i.e., the statements
that are equivalent to formulas of the form "not A[]".)

< />

I know. They have this triple negation law
           not not not P[] implies not P[]

For the propositional calculus it had been proved by {/L}kasiewicz in 1953. In the paper he claims that
the intuitionistic logic is _stronger_ that the classical one (he mentions that earlier he believed that is the other way around).
I do not cite his paper, I have only Polish translation. Maybe it would be easier for you to get the original paper and cite him.  

Jan {/L}ukasiewicz, On the intuitionistic theory of deduction. Indagationes Mathematicae. Koninklijke Nederlandse
Akademie van Wetenschappen, Proceedings, Series A, (1953), no. 2, p.113.