Почему ghci desugar type перечисляет и типы семейств? Может ли это быть выборочно отключено?

Я пытаюсь сделать типы ghci-дисплеев для моих библиотек максимально интуитивными, но я сталкиваюсь с множеством трудностей при использовании более продвинутых функций типа.

Скажем, у меня есть этот код в файле:

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

import GHC.TypeLits

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

Я загружаю его в ghci, затем набираю следующую команду:

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

К сожалению, ghci дает мне довольно уродливый вид:

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

ghci удалил сахар для строк уровня. Есть ли способ предотвратить ghci от этого и дать мне просто прекрасную версию?

В соответствующей заметке можно сказать, что я создаю функцию уровня Replicate

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

Теперь, когда я спрашиваю ghci для типа с помощью LotsOfStrings:

ghci> :t undefined :: Container LotsOfStrings

ghci хорош и дает хороший результат:

undefined :: Container LotsOfStrings

Но если я попрошу версию Replicate d,

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

ghci заменяет тип семейства, когда он не делает этого для синонима типа:

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

Почему ghci выполняет подстановку для семейства типов, но не синоним типа? Есть ли способ контролировать, когда ghci выполнит замену?

Ответы

Ответ 1

Обходной путь, который я знаю, использует: kind. Например,

ghci > : kind (Контейнер '[String, String, String, String, String])

дает:

(Контейнер '[String, String, String, String, String]):: *

В то время как

ghci > : kind! (Контейнер '[String, String, String, String, String])

Выведет что-то вроде этого:

Контейнер

(( ':)

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

Официально, конечно, вы задаете ghci другой вопрос с kind, но он работает. Использование undefined :: - это своего рода обходное решение, поэтому я думал, что этого может быть достаточно.

Ответ 2

Это исправлено в предстоящем GHC 7.8.

GHC 7.6 печатает виды, если тип данных использует PolyKinds. Таким образом, вы видите (':) * String ('[] *) вместо (':) String '[].

В GHC 7.8 виды больше не отображаются по умолчанию, и ваш тип данных довольно напечатан как список, как и следовало ожидать. Вы можете использовать новый флаг -fprint-explicit-kinds для просмотра явных видов, как в GHC 7.6. Я не знаю причин для этого, предположительно явные виды должны были помочь понять PolyKinds.

Ответ 3

import GHC.TypeLits

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

Я загружаю его в ghci, затем набираю следующую команду:

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