opciones - ¿Es posible obtener el error de tipo infinito en Haskell 98?

pattern matching haskell

Question

Estoy implementando un sistema tipo para un nuevo lenguaje de programación funcional y actualmente estoy escribiendo la función para unificar dos tipos. Hay cuatro casos que dos consideran:

+---------+---------+-------------------------------------------------------+
|   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. Cuando tanto k1 como k2 son variables, se instancian entre sí.
2. Cuando solo k1 es una variable, se crea una instancia de k2 si k1 no ocurre en k2 .
3. Cuando solo k2 es una variable, se crea una instancia de k1 si k2 no ocurre en k1 .
4. De lo contrario, verificamos si k1 y k2 tienen el mismo nombre y aridad, y unificamos sus respectivos argumentos.

Para el segundo y tercer caso necesitamos implementar la verificación de ocurrencias para no quedarnos atascados en un bucle infinito. Sin embargo, dudo que un programador pueda construir un tipo infinito en absoluto.

En Haskell, es fácil construir un tipo infinito:

let f x = f

Sin embargo, no he podido construir un tipo infinito, no importa cuánto lo intenté. Tenga en cuenta que no hice uso de las extensiones de idioma.

La razón por la que estoy preguntando esto es porque si no es posible construir un tipo infinito en absoluto, ni siquiera me molestaré en implementar la verificación de eventos para los tipos en mi sistema tipo.

Answer 1

Otro ejemplo simple

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

Answer 2

data F f = F (f F)

En GHC 7.10.1, recibo el mensaje:

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’

El mensaje no dice que es de tipo infinito, pero eso es esencialmente lo que es cuando falla la verificación.