What happens when checking the GHC?

Question

GHC validation does not allow creating infinite types. Is it advisable to prevent common errors in the code, or to prevent circular cyclic type reversal, or both?

What cases does he identify and can a malicious user trick him (as in the context of Safe Haskell) into a loop? If the type system is completed completely (is this?), I don’t understand how the GHC can guarantee that the calculation will stop.

Answer 1

Think of the type of inference as solving a system of equations. Let me take a look at an example:

fx = (x,2) 

How can we infer type f ? We see that this is a function:

 f :: a -> b 

In addition, the structure f shows that the following equations simulate:

 b = (c,d) d = Int c = a 

Solving this system of equations, we see that the type f is equal to a -> (a, Int) . Now consider the following (erroneous) function:

 fx = x : x 

Type (:) is equal to a -> [a] -> [a] , so this generates the following system of equations (simplified):

 a = a a = [a] 

So, we get the equation a = [a] , from which we can conclude that this system of equations has no solution, so the code is not well typed. If we did not reject the equation a = [a] , we would really go into an infinite loop, adding to our system the equations a = [a] , a = [[a]] , a = [[[a]]] and t .d. Etc. (Alternatively, as Daniel points out in his answer, we could allow infinite types in our type system, but that would make erroneous programs like fx = x : x for typecheck).

You can also check this in ghci:

 > let fx = x : x <interactive>:2:15: Occurs check: cannot construct the infinite type: a0 = [a0] In the second argument of `(:)', namely `x' In the expression: x : x In an equation for `f': fx = x : x 

As for your other questions: the GHC Haskell type system is not Turing-complete and the typechecker is guaranteed to stop - unless you turn on UndecidableInstances , in which case it could theoretically go in an infinite loop. However, the GHC provides termination using the recursion stack with a fixed depth, therefore it is impossible to create a program on which it never stops ( edit: according to the CAMcCann comment, this is possible in the end - there is an analog of tail recursion at the type level that allows you to loop without increasing stack depth).

Nevertheless, it is possible to compile arbitrarily for a long time, since the complexity of Hindley-Milner type inference is exponential in the worst (but not average!) Case:

 dup x = (x,x) bad = dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup . dup 

Safe Haskell does not protect you from this - see mueval if you want to allow potentially malicious users to compile Haskell programs on your system.

Answer 2

GHC validation does not allow creating infinite types.

This is true only in the most literal sense of preventing syntactically infinite types. What really happens here is just a recursive type in which the unification algorithm will need, in a sense, to embed recursion.

You can always define exactly the same type by making recursion explicit. This can be done in general using a level type fix at the level level:

 newtype Fix f = Fix (f (Fix f)) 

As an example, the type Fix ((->) a) equivalent to unifying b with (a -> b) .

In practice, however, "infinite type" errors almost always indicate an error in the code (therefore, if it breaks, you probably shouldn't fix it). A common scenario is to mix the order of the arguments or otherwise with an expression in the wrong place in code that does not use explicit types.

A type inference system that was extremely naive in the right way could potentially extend recursion until the memory runs out, but the problem of stopping is not part of it - if the type has to integrate with a part of itself that will never work ( at least in Haskell, there may be languages ​​that instead regard it as the equivalent of the explicitly recursive newtype above).

Neither type checking nor type inference in GHC is terminating unless you include UndecidableInstances , in which case you can perform arbitrary calculations through functional dependencies or family types.

Safe Haskell does not enter a picture at all. It is easy to create very large inferred types that will exhaust the system memory, even though they are finite, and if the memory helps me, Safe Haskell does not limit the use of UndecidableInstances in any case.

Answer 3

I have the following wonderful letters in my notes: There is nothing wrong with endless types! Even with infinite types, there is no real danger of making a typechecker loop. The type system is not a complete Turing (unless you explicitly ask for it to be with something like an UndecidableInstances extension).

Answer 4

The goal (in Haskell compilers) is to prevent common code errors. You can build a type checker and an output engine that will support infinite recursion of types. There is additional information in this question .

OCaml implements recursive types with -rectypes , so this is definitely possible. The OCaml community will be much more aware of some issues that arise (by default, this is disabled by default).

In the verification, extensions of an infinite type are identified. For example, this code:

 Prelude> let a = [a] <interactive>:2:10: Occurs check: cannot construct the infinite type: t0 = [t0] In the expression: a In the expression: [a] In an equation for `a': a = [a] 

if you try to determine the type manually, the type is [ [ [ [ ... ] ] ] ] . It is not possible to write such types manually because they are infinite.

Verification occurs when a type is called, which is a separate type verification step. Infinite types must be inferred because they cannot be annotated manually. Haskell-98 type output is solvable , so it is impossible to trick the compiler into a loop (error prohibition, of course, which I suspect this example uses). By default, GHC uses a limited subset of System F, for which type inference is also decidable. With some extensions, such as RankNTypes , GHC allows code for which type inference is unsolvable, but then requires type annotation, so again there is no danger of a type inference loop cycle.

Since the complete Turing languages ​​are unsolvable, the default type system cannot be completed. I don’t know if the GHC type system will be completed, with some combination of extensions, but some extensions (for example, UndecidableInstances ) allow writing code that will cause the compiler to crash with a stack overflow.

By the way, the main problem with disabling verification is that many common coding errors lead to errors of an infinite type, so disabling it usually leads to more problems than it solves. If you intend to use an infinite type, the newtype wrapper will allow no extra notes.