Hi!
Thanks Connor, I enjoyed your answer, it was very illustrative.
but then, it would be too easy to write this in haskell:
coerce :: a - b
coerce x = undefined
As an obvious consequence, Haskell type system would be unsound.
So, I assumed that this would be a wrong interpretation.
This is the part of your email which frightens me the most. Of
course Haskell's type system is unsound! What factors lead you to
this kind of assumption?
Clearly a misconception of mine.
Is it a good excuse that people told me that (or I misunderstood them) :) ?
The type system does not become a logic until you populate some of
the types (hopefully only those corresponding to true propositions)
with the terms which describe the construction of proofs. You can't
pretend that Haskell is sound just by hoping that Curry and Howard
(when properly interpreted) won't be able to see the broken bits.
It's nonetheless an interesting question which bits you need to
throw away to get a sound language. You'll have to get rid of
y :: (p - p) - p
unJust :: Maybe wmd - wmd
and hence the programming language features which enable them to
be constructed, in particular, pattern matching with incomplete
coverings, and general recursion.
Yes, I thought about those implications, that's why I also thought (incorrectly) that
it would be too limiting and therefore probably wrongly interpreted.
It is also, not too hard to see, as you said, that general recursion would validate
that interpretation (even without using any other primitives or functions):
coerce :: a - b
coerce = coerce
or even
coerce :: a - b
coerce x = let y = y in y
Then, even if we ignored the primitives, Haskell would still be unsound!
Moreover, we could then say that most of the functional languages (which have a
similar type system) are unsound.
Right ? Is it Charity an exception on this?
There's an interesting paper `Elementary Strong Functional
Programming' by David Turner, in which he proposes such a language.
He suggests that, at least for paedagogical purposes, a functional
language which gave up completeness for consistency might be no
bad thing. I'm inclined to agree with him.
I will take a look on it.
So I won't make any foolish and portentous pronouncements about
dependent types being the only way to save us from damnation. I'll
merely observe that we often use the unsound parts of programming
languages as the best approximations available to the programs
we really mean: we don't intend recursion to loop infinitely,
we just have no means to explain in the program why it doesn't;
we don't intend to apply unJust to Nothing, we just have no means
to explain in the program why this can't happen. Dependent types
support a higher level of articulacy about what is really going on,
reducing, but not removing entirely the need to work outside the
consistent fragment of the language. They do not save us from Satan
but from Wittgenstein. Whereon you know something, thereon speak!
Dependent types definitely seem an advance to me. I saw recently a presentation
of a very impressive tool (epigram - I wonder if you have heard about it :P).
I'll be definitely take a better look on it as soon as I finish some work with more
priority.
Best Regards,
Bruno
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
