Checking completion in functional programs

Question

Are there functional languages ​​that can be specified in the typechecker method, is a certain calculation guaranteed to complete? Or can you only do this in Haskell?

Regarding Haskell, in this answer , the poster says that

The usual way to think about this is that each Haskell type is "removed" - it contains ⊥. That is, Bool matches {⊥, True, False} , and not just {True, False} . This means that Haskell programs do not guarantee termination and may have exceptions.

On the other hand, this Agda article says that

The right Agda program is one that passes both type checking and termination checking

Ie, all Agda programs will end, and a Bool in Agda matches exactly {True, False} .

So, for example, in Haskell, you can have a value of type IO a , which tells typechecker that IO is necessary to calculate the value in question. Could you be of type Lifted a , which claims that the specified calculation cannot complete? That is, you allow non-interruption, but you share it in the type system. (Obviously, as in Agda, you can only split the values ​​into "definitely ending" and "don't interrupt"). If not, are there languages ​​that do this?

Answer 1

Of course you could. However, this would not be ideal. By definition, some calculations that end should be in Lifted . This is called a stop problem.

Now, before giving up on this idea, it doesn't sound so bad. Coq, Agda and many others work fine with heuristics to verify completion.

Languages ​​where it really matters are found in languages ​​like Coq and Agda, where you are trying to prove theorems. For example, suppose we are of type

  Definition falsy := exists n, n > 0 /\ 0 > n. -- Read this as, -- "The type of a proof that for some number n, n > 0 and n < 0" 

In the syntax of Coq. /\ means and. Now, to prove such a property in Coq or Agda, we need to write something like

 Definition out_proof : falsy = ____. -- Read this as -- "A proof that there exists a number n < 0 and n > 0" 

Where ____ is proof that for some number n , n > 0 and 0 > n . Now this is terribly complicated, as well, falsy is false. Obviously, there is no number that is less than and greater than 0.

However, if we allowed iteration with unlimited recursion,

  Definition bottom_proof : falsy = bottom_proof. 

This type checks, but is clearly inconsistent! We just proved something false! Thus, the proof-of-concept assistants prove that some form of verification of completion, otherwise they are useless.

If you want to be pragmatic, you can use this elevated type to basically say that it is a sticker program: "Back, I know that this may not end, but I'm fine." This is useful for writing real-world material, such as, say, a web server or any other place where you might want to run it forever.

In essence, you are proposing a separation in this language, on the one hand, you have a “proven code” that you can talk about about it calmly, and on the other, an “unsafe code” that can go in cycles forever. You are right when comparing with IO . This is exactly the same idea as splitting side effects on Haskell.

Edit: Core data

You mentioned corrective data, but that’s not exactly what you want. The idea is that you do the cycle forever, but you do it "productively." In essence, with recursion, the easiest way to verify that you are completing is that you always recurs with a term strictly less than what you currently have.

 Fixpoint factorial n := match n with | 0 => 1 | S n' => n * factorial n' 

With corecursion, your final term should be "more" than your input.

 Cofixpoint stream := Cons 1 stream 

Again it does not allow

  Cofixpoint stream := stream