Verificación de tipos dentro de las cuasi comillas en la plantilla Haskell

types metaprogramming

Question

Estoy tratando de familiarizarme con Template Haskell , y para mi sorpresa, el siguiente código se compila bajo ghc (versión 6.10.4).

main = do let y = [| "hello" + 1 |] putStr ""

Esto me sugiere que no hay ninguna comprobación de tipos dentro de las casi comillas. Esto no es lo que hubiera esperado después de leer el paper original en Template Haskell. Además el siguiente programa no compila.

main = do let y = [| "hello" && True |] putStr ""

¿Que está pasando aqui?

Answer 1

Parece que GHC escribe todas las citas pero asume que se pueden satisfacer todas las restricciones de instancia generadas.

En este código:

main = do
let
y = [| "hello" + 1 |]
putStr ""

El corchete y es tipeable bajo el supuesto de que tenemos una instancia de Num String. Dado que GHC no puede decir con seguridad que no se presentará una instancia de este tipo antes de que se empalme, no da un error de tipo.

En este código:

 main = do
let
y = [| "hello" && True |]
putStr ""

No hay forma de que y pueda ser empalmado con éxito, sin importar el entorno de instancia que configure.

Este es solo un ejemplo de cómo el mecanismo de comprobación de tipos de Template Haskell es demasiado indulgente. Otros ejemplos se analizan en la publicación del blog de Simon PJ en http://hackage.haskell.org/trac/ghc/blog/Template%20Haskell%20Proposal , donde propone un cambio para no teclear chequee ninguna cita en absoluto.

Answer 2

Plantilla Haskell tiene dos operaciones principales:

• levantamiento: [| |] [| |]
• empalme $( )

Cuando ajusta algo en los corchetes de Oxford, retrasa la verificación de su tipo (y la evaluación) y, en su lugar, crea un fragmento AST que se verificará cuando se vuelva a empalmar.

El AST que se construye se puede observar:

{-# LANGUAGE TemplateHaskell #-}
import Language.Haskell.TH
main = print =<< runQ [| "hello" + 1 |]

Ejecutando este programa (o escribiendo la expresión del corchete en GHCi), obtenemos un AST bien formado, pero uno que no es correcto si se trata como un fragmento de Haskell:

InfixE (Just (LitE (StringL "hello"))) (VarE GHC.Num. +) (Just (LitE (IntegerL 1)))

Ahora, cuando intentamos realmente empalmarlo, la comprobación de tipos ocurre:

*Main> :t [| "hello" + 1 |]
[| "hello" + 1 |] :: Q Exp
*Main> $( [| "hello" + 1 |] )
<interactive>:1:4:
No instance for (Num [Char])
arising from the literal `1''

Como esperamos. Entonces, sí, las expresiones TH son de tipo comprobado, pero en un punto tardío, cuando se empalman nuevamente en un programa.