¿Por qué ghci desugar escribe listas y familias de tipos? ¿Se puede desactivar selectivamente?

93

Estoy tratando de hacer que los tipos de visualización de ghci para mis bibliotecas sean lo más intuitivos posible, pero me encuentro con muchas dificultades al utilizar funciones de tipo más avanzadas.

Digamos que tengo este código en un archivo:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeLits

data Container (xs::[*]) = Container

Lo cargo en ghci, luego escribo el siguiente comando:

ghci> :t undefined :: Container '[String,String,String,String,String]

Desafortunadamente, ghci me da un aspecto bastante feo:

:: Container
       ((':)
          *
          String
          ((':)
             * String ((':) * String ((':) * String ((':) * String ('[] *))))))

ghci ha eliminado el azúcar para las cadenas de nivel de tipo. ¿Hay alguna forma de evitar que ghci haga esto y me dé la versión bonita?

En una nota relacionada, digamos que creo una Replicatefunción de nivel de tipo

data Nat1 = Zero | Succ Nat1

type family Replicate (n::Nat1) x :: [*]
type instance Replicate Zero x = '[]
type instance Replicate (Succ n) x = x ': (Replicate n x)

type LotsOfStrings = Replicate (Succ (Succ (Succ (Succ (Succ Zero))))) String

Ahora, cuando le pregunto a ghci por un tipo usando LotsOfStrings:

ghci> :t undefined :: Container LotsOfStrings

ghci es agradable y me da un bonito resultado:

undefined :: Container LotsOfStrings

Pero si pido la Replicateversión d,

ghci> :t undefined :: Container (Replicate (Succ (Succ (Succ (Succ (Succ Zero))))) String)

ghci sustituye a la familia de tipos cuando no hizo eso para el sinónimo de tipos:

:: Container
       ((':)
          *
          [Char]
          ((':)
             * [Char] ((':) * [Char] ((':) * [Char] ((':) * [Char] ('[] *))))))

¿Por qué ghci sustituye la familia de tipos, pero no el sinónimo de tipos? ¿Hay alguna forma de controlar cuándo ghci hará la sustitución?

haskell types ghci Mike Izbicki
fuente
7
Debido a que los sinónimos de tipo están diseñados exclusivamente para el consumo humano, no realiza la sustitución porque reconoce que usted hizo el sinónimo de tipo porque quería escribir / ver el tipo de esa manera. Realiza la sustitución con la familia de tipos porque las familias de tipos realmente se tratan de calcular / deducir un tipo, no de mostrarlo.
AndrewC
La solución a su problema está en su pregunta: cree un sinónimo de tipo si desea abreviar.
AndrewC
2
@AndrewC Acabo de pensar en otra pregunta relacionada con su comentario: ¿Por qué los tipos de cadenas a veces se muestran como [Char]ya veces se muestran como String?
Mike Izbicki
1
Creo que ghci intenta preservar los sinónimos de tipo que encuentra en la fuente. Es decir, si se declara que una función es de tipo String->String, el tipo de su resultado se mostrará como String. Sin embargo, si tiene que construir un tipo a partir de piezas, como en eg "abc"(que es lo mismo que 'a':'b':'c':[]), no hay sinónimo que conservar. Esto es pura especulación.
n. 'pronombres' m.
4
@nm: Tenga en cuenta que GHC hace un intento similar de preservar los nombres de las variables de tipo, cuando los tipos inferidos más genéricos se unifican con las variables de tipo menos genéricas y con nombres explícitos. Sospecho que si el tipo explícito Stringestá unificado con variables de tipo f ao [a], se mostrará como [Char]después por razones similares.
CA McCann

Respuestas:

2

La solución alternativa que conozco está usando: kind. Por ejemplo,

ghci>: kind (Contenedor '[String, String, String, String, String])

Da:

(Contenedor '[String, String, String, String, String]) :: *

Mientras

ghci>: ¡amable! (Contenedor '[String, String, String, String, String])

Imprimirá algo como esto:

Envase

((':)

  *
  [Char]
  ((':)
     * [Char] ((':) * [Char] ((':) * [Char] ((':) * [Char] ('[] *))))))

Oficialmente, por supuesto, le estás haciendo a ghci una pregunta diferente kind, pero funciona. El uso undefined ::es una especie de solución alternativa de todos modos, así que pensé que esto podría ser suficiente.

usuario2141650
fuente
Solo estaba usando undefined ::para dar un ejemplo fácil. El problema real es cuando recibe un mensaje de error que tiene el tipo de una lista de mil tipos diferentes. Se necesitan páginas para imprimirlo y es muy difícil de analizar.
Mike Izbicki
Sí, bastante justo. Podría haberse dado cuenta de eso. Te debo una mejor respuesta
user2141650
2

Esto se soluciona en la próxima GHC 7.8.

GHC 7.6 imprime tipos si un tipo de datos usa PolyKinds. Entonces ves en (':) * String ('[] *)lugar de solo (':) String '[].

En GHC 7.8, los tipos ya no se muestran de forma predeterminada y su tipo de datos está bastante impreso como una lista, como era de esperar. Puedes usar la nueva bandera-fprint-explicit-kinds para ver tipos explícitos como en GHC 7.6. No sé las razones de esto, presumiblemente los tipos explícitos estaban destinados a ser una ayuda para comprender PolyKinds.

sdcvvc
fuente
0 
import GHC.TypeLits

data Container (xs::[*]) = Container

Lo cargo en ghci, luego escribo el siguiente comando:

:t undefined :: Container '[String,String,String,String,String]
ئیترده ڕۆم
fuente
Entonces...? Supongo que todavía obtienes el resultado sin azúcar, es decir String ((':) * String ((':) * String ((':) * ....
izquierda rotonda alrededor del