On Tue, 16 Feb 1999, S. Alexander Jacobson wrote:
> I read cayenne.ps and it went somewhat over my head.
> I could not get a good sense of when in practice I would really want to use
> this. This is not an objection, just a request for explanation...
>
[snip]
This is a tough one, but i will try to give my view of dependent types:
(As i have just played around with cayenne, for a short while, I probably
have not yet understood the full benefit).
Going from hindley milner to dependent types, is a bit like going from C
to haskell. Understanding the benefits of dependent types requires you to
think in another way than you are used to!
Dependent types rests on a solid foundation of Martin Löf's type theory,
and the curry-howard isomorphism.
The isomorphism says that a type can be seen as a logical proposition, and
a (complete) function with a particular type can be seen as a constructive
proof of the corresponding proposition.
Proposition: Type: Comment:
A and B (A,B) Product
A or B Either A B Sum
A implies B A -> B
Exists x A(x) . ADT
. .
. .
Look at the following function:
fst :: (a,b) -> a
fst (a,b)
The type signature cooresponds to the proposition (A and B) implies A.
The implementation is a trivial proof using And-elimination in natural
deduction.
So this suggests a design methodology for developing software systems:
1. Specifying the system and the required properties of the system:
Write type signatures of functions.
2. Implementing the system:
Write the implementation of the function.
3. *Prove* that the implementation is correct:
Typecheck the program. (Only a valid proof if all functions are total)
>On Tue, 16 Feb 1999, S. Alexander Jacobson wrote:
> I read cayenne.ps and it went somewhat over my head.
> I could not get a good sense of when in practice I would really want to use
> this. This is not an objection, just a request for explanation...
>
[snip]
This is a tough one, but i will try to give my view of dependent types:
(As i have just played around with cayenne, for a short while, I probably
have not yet understood the full benefit).
Going from hindley milner to dependent types, is a bit like going from C
to haskell. Understanding the benefits of dependent types requires you to
think in another way than you are used to!
Dependent types rests on a solid foundation of Martin Löf's type theory,
and the curry-howard isomorphism.
The isomorphism says that a type can be seen as a logical proposition, and
a (complete) function with a particular type can be seen as a constructive
proof of the corresponding proposition.
Proposition: Type: Comment:
A and B (A,B) Product
A or B Either A B Sum
A implies B A -> B
Exists x A(x) . ADT
. .
. .
Look at the following function:
fst :: (a,b) -> a
fst (a,b)
The type signature cooresponds to the proposition (A and B) implies A.
The implementation is a trivial proof using And-elimination in natural
deduction.
So this suggests a design methodology for developing software systems:
1. Specifying the system and the required properties of the system:
Write type signatures of functions.
2. Implementing the system:
Write the implementation of the function.
3. *Prove* that the implementation is correct:
Typecheck the program. (Only a valid proof if all functions are total)
>On Tue, 16 Feb 1999, S. Alexander Jacobson wrote:
> I read cayenne.ps and it went somewhat over my head.
> I could not get a good sense of when in practice I would really want to use
> this. This is not an objection, just a request for explanation...
>
[snip]
This is a tough one, but i will try to give my view of dependent types:
(As i have just played around with cayenne, for a short while, I probably
have not yet understood the full benefit).
Going from hindley milner to dependent types, is a bit like going from C
to haskell. Understanding the benefits of dependent types requires you to
think in another way than you are used to!
Dependent types rests on a solid foundation of Martin Löf's type theory,
and the curry-howard isomorphism.
The isomorphism says that a type can be seen as a logical proposition, and
a (complete) function with a particular type can be seen as a constructive
proof of the corresponding proposition.
Proposition: Type: Comment:
A and B (A,B) Product
A or B Either A B Sum
A implies B A -> B
Exists x A(x) . ADT
. .
. .
Look at the following function:
fst :: (a,b) -> a
fst (a,b) = a
The type signature cooresponds to the proposition (A and B) implies A.
The implementation is a trivial proof using And-elimination in natural
deduction.
So this suggests a design methodology for developing software systems:
1. Specifying the system and the required properties of the system:
Write type signatures of functions.
2. Implementing the system:
Write the implementation of the function.
3. *Prove* that the implementation is correct:
Typecheck the program. (Only a valid proof if all functions are total)
>On Tue, 16 Feb 1999, S. Alexander Jacobson wrote:
> I read cayenne.ps and it went somewhat over my head.
> I could not get a good sense of when in practice I would really want to use
> this. This is not an objection, just a request for explanation...
>
[snip]
This is a tough one, but i will try to give my view of dependent types:
(As i have just played around with cayenne, for a short while, I probably
have not yet understood the full benefit).
Going from hindley milner to dependent types, is a bit like going from C
to haskell. Understanding the benefits of dependent types requires you to
think in another way than you are used to!
Dependent types rests on a solid foundation of Martin Löf's type theory,
and the curry-howard isomorphism.
The isomorphism says that a type can be seen as a logical proposition, and
a (complete) function with a particular type can be seen as a constructive
proof of the corresponding proposition.
Proposition: Type: Comment:
A and B (A,B) Product
A or B Either A B Sum
A implies B A -> B
Exists x A(x) . ADT
. .
. .
Look at the following function:
fst :: (a,b) -> a
fst (a,b) = a
The type signature cooresponds to the proposition (A and B) implies A.
The implementation is a trivial proof using And-elimination in natural
deduction.
So this suggests a design methodology for developing software systems:
1. Specifying the system and the required properties of the system:
Write type signatures of functions.
2. Implementing the system:
Write the implementation of the function.
3. *Prove* that the implementation is correct:
Typecheck the program. (Only a valid proof if all functions are total)
>From a more pragmatic point of view:
a Type is a first class value.
This means that the result of a function can be a type.
f :: Int -> # -- # is the type of types
f 0 = Int
f 1 = Bool
(This function is of course just nonsense)
Sometimes a it is easiest to view a type as a domain,
sometimes as a proof object.
power :: (n::Int) -> Even n -> Int
This is a function which takes an int, and a proof that the int is even,
and returns an int. (If we define 'Even' that way)
There is a war going on between those in favour of strong and weak type
systems.
Those in favour of weak typesystems says that the type system is in the
way. It stops them from writing the programs they want to write. My view
is that a strong system is good because it offloads some burdens from the
programmer, and the machine should do as much of those boring things as
possible. A type system is 'in the way' if it is not expressive enough to
express the things you would like to write. An example:
Pascal is a strongly typed language
Haskell is a strongly typed language
In pascal you can't write a function which takes an integer array of
arbitrary size and calculates the sum. Why? Surely not because it is
strongly typed. The reason is that the type system it has can't express
the notion of arbitrary sized array, it is not expressive enough.
The point is:
1. You should have a strong type system, it should be the compilers
responsibility to detect as many errors in the source code as it can.
2. The Type system should be expressive enough, so that the programmer can
write those programs he would like to.
Dependent types put even fewer restrictions (than haskell) on what types
of programs you can write, while maintaining type safety.
/Lars L
