Halting problem solved.
Only terminated lambda terms could be expressed with specially designed GADT, within Haskell type system, of course.
Что приятно. Но сил изучать пристально, пока, нет. ;)
Что приятно. Но сил изучать пристально, пока, нет. ;)
Comments 2
On 1/8/07, Robin Green wrote:
> On Mon, 8 Jan 2007 08:51:40 -0500
> "Jim Apple" wrote:
>> GHC's type checker ends up doing exactly what it was doing before:
>> checking proofs.
>
> Well, not really - or not the proof you thought you were getting. As I
> am constantly at pains to point out, in a language with the possibility
> of well-typed, non-terminating terms, like Haskell, what you actually
> get is a "partial proof" - that *if* the expression you are demanding
> terminates, you will get a value of the correct type.
Of course. Were there a recursion-free dialect of Haskell, it could be
typecheck/proofcheck the Terminating datatype, though it would be
useless for doing any actual work. Proof assistants like Coq can solve
this dilemma, and so can languages in the Dependent ML family, by
allowing non-terminating programs but only terminating proofs, and by
proving termination by well-founded induction.
Nobody should think Haskell+GADTs provides the sort of assurances that
these can.
Reply
Reply
Leave a comment