haskell - mac - ¿Por qué ghci desugar type enumera y escribe familias? ¿Se puede deshabilitar selectivamente?

haskell full

Question

Estoy tratando de hacer que los tipos de pantallas ghci para mis bibliotecas sean lo más intuitivos posible, pero me encuentro con muchas dificultades cuando uso 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 una apariencia bastante fea:

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

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

En una nota relacionada, digamos que creo una función Replicate 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 pido a ghci un tipo usando LotsOfStrings :

ghci> :t undefined :: Container LotsOfStrings

ghci es agradable y me da el resultado bonito:

undefined :: Container LotsOfStrings

Pero si solicito la versión Replicate 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 tipo:

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

¿Por qué está haciendo ghci la sustitución de la familia tipo, pero no el tipo sinónimo? ¿Hay alguna manera de controlar cuándo ghci hará la sustitución?

Answer 1

Esto se soluciona en el próximo GHC 7.8.

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

En GHC 7.8, los tipos ya no se muestran por defecto y su tipo de datos está bastante impreso como una lista, como era de esperar. Puede usar el nuevo -fprint-explicit-kinds para ver tipos explícitos como en GHC 7.6. No sé las razones para esto, supuestamente los tipos explícitos estaban destinados a ser una ayuda para entender PolyKinds.

Answer 2

La solución que yo conozco está usando: amable. Por ejemplo,

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

Da:

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

Mientras

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

Se imprimirá algo como esto:

Envase

(('':)

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

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

Answer 3

import GHC.TypeLits

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

Lo cargo en ghci, luego escribo el siguiente comando:

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