È possibile ottenere l'errore di tipo infinito in Haskell 98?

Question

Sto implementando un sistema gentile per un nuovo linguaggio di programmazione funzionale e sto attualmente scrivendo la funzione per unificare due tipi. Ci sono quattro casi due in considerazione:

+---------+---------+-------------------------------------------------------+ 
| k1 | k2 |      action       | 
+=========+=========+=======================================================+ 
| var | var |     k1 := k2^k2 := k1     | 
+---------+---------+-------------------------------------------------------+ 
| var | non var |    if (!occurs(k1, k2)) k1 := k2    | 
+---------+---------+-------------------------------------------------------+ 
| non var | var |    if (!occurs(k2, k1)) k2 := k1    | 
+---------+---------+-------------------------------------------------------+ 
| non var | non var | ensure same name and arity, and unify respective args | 
+---------+---------+-------------------------------------------------------+ 

1. Quando sia k1 e k2 sono variabili poi sono istanziati gli uni agli altri.
2. Quando solo k1 è una variabile, viene istanziata a k2 iff k1 non si verifica in k2.
3. Se solo k2 è una variabile, viene istanziato a k1 se non si verifica k2 in k1.
4. Altrimenti verifichiamo se k1 e k2 hanno lo stesso nome e arità e unificare i rispettivi argomenti.

Per il secondo e il terzo caso è necessario implementare il controllo di verifica in modo da non rimanere bloccati in un ciclo infinito. Tuttavia, dubito che un programmatore sia in grado di costruire un tipo infinito.

In Haskell, è facile da costruire un tipo di infinito:

let f x = f 

Tuttavia, non sono stati in grado di costruire un tipo infinito non importa quanto duramente ho provato. Nota che non ho usato alcuna estensione di lingua.

La ragione per cui sto chiedendo questo è perché se non è possibile costruire un tipo infinito, allora non mi preoccuperò nemmeno di implementare il controllo dei casi nel mio sistema gentile.

Answer 1

data F f = F (f F) 

Su GHC 7.10.1, ottengo il messaggio:

kind.hs:1:17: 
    Kind occurs check 
    The first argument of ‘f’ should have kind ‘k0’, 
     but ‘F’ has kind ‘(k0 -> k1) -> *’ 
    In the type ‘f F’ 
    In the definition of data constructor ‘F’ 
    In the data declaration for ‘F’ 

Il messaggio non dice che è un tipo infinita, ma questo è essenzialmente quello che è quando la verifica controllo ha esito negativo.

Answer 2

Un altro semplice esempio

GHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help 
Prelude> let x = undefined :: f f 

<interactive>:2:24: 
    Kind occurs check 
    The first argument of ‘f’ should have kind ‘k0’, 
     but ‘f’ has kind ‘k0 -> k1’ 
    In an expression type signature: f f 
    In the expression: undefined :: f f 
    In an equation for ‘x’: x = undefined :: f f