type theory and higher order logic? : Functional

On Thu, 08 Feb 2007 10:35:51 +0100, Dirk Thierbach wrote:

> The more expressive
> your type system is, the more you can say about your programs, but
> the harder it gets to do type inference or type checking.

Harder how? More compute time in the compile (which just requires
more/faster silicon), or more complexity in the inferer/checker (which
requires cleverer humans/real work)?

What is the limit? Is there one?

Cheers,

--
Andrew

Andrew Reilly <andrew-newspost@areilly.bpc-users.org> writes:

> On Thu, 08 Feb 2007 10:35:51 +0100, Dirk Thierbach wrote:
>
>> The more expressive
>> your type system is, the more you can say about your programs, but
>> the harder it gets to do type inference or type checking.
>
> Harder how? More compute time in the compile

Yes.

> (which just requires more/faster silicon),

No.

> or more complexity in the inferer/checker

Yes.

> (which requires cleverer humans/real work)?

No. The problem seems to algorithmic complexity not implementation.

> What is the limit? Is there one?

Probably not.

Rumour has it (I haven't checked) that some GHC extensions of the
Haskell type system just don't terminate if the programm is not well
typed.

Regards -- Markus

Andrew Reilly <andrew-newspost@areilly.bpc-users.org> wrote:
> On Thu, 08 Feb 2007 10:35:51 +0100, Dirk Thierbach wrote:

>> The more expressive your type system is, the more you can say about
>> your programs, but the harder it gets to do type inference or type
>> checking.

> Harder how? More compute time in the compile (which just requires
> more/faster silicon), or more complexity in the inferer/checker (which
> requires cleverer humans/real work)?

The latter.

> What is the limit? Is there one?

Typing can quickly become undecidable if the type system is expressive
enough. One can live even with that to some degree by imposing
external restriction (e.g. "give up after so many attempts"), but
that's not pretty.

- Dirk

Andrew Reilly schrieb:
> On Thu, 08 Feb 2007 10:35:51 +0100, Dirk Thierbach wrote:
>
>> The more expressive
>> your type system is, the more you can say about your programs, but
>> the harder it gets to do type inference or type checking.
>
> Harder how? More compute time in the compile (which just requires
> more/faster silicon), or more complexity in the inferer/checker (which
> requires cleverer humans/real work)?

Both, actually.
As the type system becomes more powerful, the algorithms get slower.
This affects both worst-case and average complexities.

There's another problem: the more complex a type system is, the more
difficult it is to represent a type in an error message like "found type
X, expected type Y". There are situations where the representation of X
and Y is longer than the program.

Regards,
Jo

In article <7x7iut70rq.fsf@ruckus.brouhaha.com>, Paul Rubin wrote:
>
> Do humans use higher than second order logic? I gather 2-OL allows
> quantification over sets, and 3-OL allows quantification over
> relations.

You can quantify over relations in second order logic, since a
relation is just a binary predicate symbol. So R(a,b) says a relation
holds between a and b.

If we write down a grammar of sorts as follows, with X standing for
the sort of individuals, prop standing for propositions, and
the function space ==> between them:

s ::= X | prop | s -> s

Now, a first order logic only permits quantification over X. Second
order logic permits quantification over any sort, including function
sorts, but restricts prop to appear only at the base of the sort.
Examples of such sorts are:

X
prop
X -> prop
X -> X -> prop

The last two lines correspond to quantification over predicates and
over relations. Note that the restriction of second order-logic is
that you can't have quantifications over things like (prop -> prop) or
(X -> prop) -> prop, because a prop appears somewhere other than the
base of the sort. A higher order logic allows quantification at any
order, with no restrictions on where prop can appear in a sort.

The concept of a logical operator is an example of a third order
concept -- the theorem asserting the existing of the negation operator
might be stated in higher-order logic as:

exists not : prop -> prop.
forall P : prop.
P implies (not P) implies false

> But we're taught in school that relations are just sets of ordered
> pairs, and we really do think of them that way; it's not an
> artificial construction like thinking of natural numbers as von
> Neumann ordinals.

You may, but I don't. I think of relations as n-ary predicates, and
predicates are logical primitives for me. Treating them as sets of
ordered pairs is a way of giving semantics to certain relations, but
the concept of a relation is prior to that semantics.

As an example, note that the membership relation "x in S" is defined
for all sets S, which would lead to a circularity if the membership
relation were itself a set of pairs.

> I'd like to tie this stuff back to programming though. What little
> logic I know is from math class, and programmers (I mean those
> working with software proofs etc.) seem to approach it differently.
> Is there good stuff to read online?

PL researchers tend to have a lot more sympathy for constructive
and proof-theoretic methods than is normal. Jean-Yves Girard's
book _Proofs and Types_ is probably a good place to look. It's
online at:

<http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html>


--
Neel R. Krishnaswami
neelk@cs.cmu.edu

Dirk Thierbach wrote:
> Paul Rubin <http://phr.cx@nospam.invalid> wrote:
>> Neelakantan Krishnaswami <neelk@cs.cmu.edu> writes:
>>> Thanks to Curry-Howard, a type system is a logic. If you have a rich
>>> logic (eg, higher order logic), then you can express definitions much
>>> more succintly and naturally than you can in a weaker one. This makes
>>> the task of formalization easier, because the human user of the system
>>> can keep his or her definitions and proofs closer to the mathematics.
>
>> I'd like to tie this stuff back to programming though. What little
>> logic I know is from math class, and programmers (I mean those working
>> with software proofs etc.) seem to approach it differently.
>
> Programmers nearly always want to express information about the
> programs they write> They just do it in different ways, and call it
> unit tests, or pre- and postconditions, or other things. A type system
> is just another way to express such information. With the additional
> benefit that you have an "automatic theorem prover" (the compiler)
> which checks statically that what you say about your program really
> holds, always, no matter what actual values you use when the program
> runs.

I think it would be more accurate to describe what the compiler does here
as "proof checker" rather than "theorem proover". The compiler doesn't
automatically write the code of a function if you give it a type signature.
Rather it automatically checks that your implementation of a function is a
valid proof of what the type signature proposes.

Cheers
Ben

Neelakantan Krishnaswami wrote:
>> But we're taught in school that relations are just sets of ordered
>> pairs, and we really do think of them that way; it's not an
>> artificial construction like thinking of natural numbers as von
>> Neumann ordinals.
>
> You may, but I don't. I think of relations as n-ary predicates, and
> predicates are logical primitives for me. Treating them as sets of
> ordered pairs is a way of giving semantics to certain relations, but
> the concept of a relation is prior to that semantics.
>
> As an example, note that the membership relation "x in S" is defined
> for all sets S, which would lead to a circularity if the membership
> relation were itself a set of pairs.

Wow, thank you very much! With these two short paragraphs you clarified a
question I have been asking myself for a very long time.

Could you elaborate a bit on your statement that "treating them [relations]
as sets of ordered pairs is a way of giving semantics to certain
relations"? What does it mean to give semantics to a relation?

Thanks
Ben

In article <eqga9p$1rbp$1@ulysses.news.tiscali.de>, Benjamin Franksen wrote:
>
> Wow, thank you very much! With these two short paragraphs you
> clarified a question I have been asking myself for a very long time.
>
> Could you elaborate a bit on your statement that "treating them
> [relations] as sets of ordered pairs is a way of giving semantics to
> certain relations"? What does it mean to give semantics to a
> relation?

If you believe in some mathematics already -- usually people say they
believe in ZFC set theory (though I am agnostic on that point) --
"giving a semantics to a relation" means that you explain what a
relation is and how to use it in terms of the stuff you already
believe in.

So suppose we want to formalize the idea of less-than over the natural
numbers, which I'll write as x < y. We have an intuitive idea of what
this should and shouldn't let us deduce, and if we formalize the idea
in set theory we can start using the idea freely. So, suppose that we
have the von Neumann natural numbers:

0 == {}
1 == {0}
2 == {0, 1}
3 == {0, 1, 2}
....

Note that each natural number contains all the naturals smaller than
it. So we decide to exploit this fact to define a new set, which we'll
call <:

< == { (x,y) in N x N | x in y }

Now, we say that x < y if the pair (x,y) is in the set <.

Then, we can prove that x < y satisfies the properties we intuitively
believe it should -- that it is transitive, and that for every x and y,
either x < y, y < x, or x == y, and so on.

So basically we've explained how to define an intuition in terms of
math we already knew, and then proved that this definition satisfies
the properties that we believed should hold. That's what it means to
give a semantics.

On the other hand, suppose that it turned out that this definition
didn't match our intuitions. Now we face a choice: we can either
conclude that our formalization is inadequate, and look for a better
formalization, or we can change our minds about what our intuitions
should be. In practice, mathematicians do both -- you write
definitions to formalize your intuitions, and then adjust both your
formalizations and your intuitions until they are in harmony.



--
Neel R. Krishnaswami
neelk@cs.cmu.edu

Benjamin Franksen <benjamin.franksen@bessy.de> writes:
> I think it would be more accurate to describe what the compiler does here
> as "proof checker" rather than "theorem proover". The compiler doesn't
> automatically write the code of a function if you give it a type signature.
> Rather it automatically checks that your implementation of a function is a
> valid proof of what the type signature proposes.

Well, some languages use type inference to prove that functions and
their callers use compatible types, even in the absence of
user-supplied signatures. Slightly tangential: apparently in Haskell,
the inference algorithm involves unification. Any suggestions where I
can find out more about that?

Paul Rubin <http://phr.cx@nospam.invalid> wrote:
> Benjamin Franksen <benjamin.franksen@bessy.de> writes:
>> I think it would be more accurate to describe what the compiler does here
>> as "proof checker" rather than "theorem proover". The compiler doesn't
>> automatically write the code of a function if you give it a type signature.
>> Rather it automatically checks that your implementation of a function is a
>> valid proof of what the type signature proposes.

Yes, of course, if you think in terms of the Curry-Howard isomorphism.
I meant "theorem" in the sense "claim that this function really has
this type".

> Well, some languages use type inference to prove that functions and
> their callers use compatible types, even in the absence of
> user-supplied signatures.

Under the Curry-Howard view this would correspond to knowing the proof
(the program) and then inferring the theorem (the type) from it.

> Slightly tangential: apparently in Haskell, the inference algorithm
> involves unification. Any suggestions where I can find out more
> about that?

The basic Hindley-Milner type inference algorithm alread needs
unification, so almost any typed functional language will need it.
Googling for "Hindley-Milner" might turn up a more specific description.

- Dirk