Как именно работают добрые списки?

Question

Я читал на vinyl недавно, который использует странные "списки видов" своего рода типов. Прочитав немного о видах и виниле, я получил некоторое интуитивное понимание их, и я смог взломать это вместе

{-# LANGUAGE DataKinds,
             TypeOperators,
             FlexibleInstances,
             FlexibleContexts,
             KindSignatures,
             GADTs #-}
module Main where

-- from the data kinds page, with HCons replaced with :+:
data HList :: [*] -> * where
  HNil :: HList '[]
  (:+:) :: a -> HList t -> HList (a ': t)

infixr 8 :+:


instance Show (HList '[]) where
  show _ = "[]"
instance (Show a, Show (HList t)) => Show (HList (a ': t)) where
  show (x :+: xs) = show x ++ " : " ++  show xs

class ISum a where
  isum :: Integral t => a -> t

instance ISum (HList '[]) where
  isum _ = 0


instance (Integral a, ISum (HList t)) => ISum (HList (a ': t)) where
  isum (x :+: xs) = fromIntegral x + isum xs

-- explicit type signatures just to check if I got them right
alist :: HList '[Integer]
alist = (3::Integer) :+: HNil

blist :: HList '[Integer,Int]
blist =  (3::Integer) :+: (3::Int) :+: HNil

main :: IO ()
main = do
  print alist
  print (isum alist :: Int)
  print blist
  print (isum blist :: Integer)

:i HList доходность

data HList $a where
  HNil :: HList ('[] *)
  (:+:) :: a -> (HList t) -> HList ((':) * a t)
    -- Defined at /tmp/test.hs:10:6
instance Show (HList ('[] *)) -- Defined at /tmp/test.hs:17:10
instance (Show a, Show (HList t)) => Show (HList ((':) * a t))
  -- Defined at /tmp/test.hs:19:10
instance ISum (HList ('[] *)) -- Defined at /tmp/test.hs:25:10
instance (Integral a, ISum (HList t)) => ISum (HList ((':) * a t))
  -- Defined at /tmp/test.hs:29:10
*Main> :i HList
data HList $a where
  HNil :: HList ('[] *)
  (:+:) :: a -> (HList t) -> HList ((':) * a t)
    -- Defined at /tmp/test.hs:10:6
instance Show (HList ('[] *)) -- Defined at /tmp/test.hs:17:10
instance (Show a, Show (HList t)) => Show (HList ((':) * a t))
  -- Defined at /tmp/test.hs:19:10
instance ISum (HList ('[] *)) -- Defined at /tmp/test.hs:25:10
instance (Integral a, ISum (HList t)) => ISum (HList ((':) * a t))
  -- Defined at /tmp/test.hs:29:10

Из чего я понимаю, что '[] это сахар для '[] * а также x ': y за (':) * x y, Что это * делает там? Это вид элементов списка? Кроме того, что именно такой список в любом случае? Это что-то встроено в язык?

Answer 1

Тот * это... неудачно. Это результат симпатичного принтера GHC для многогранных типов данных. Это приводит к вещам, которые синтаксически недопустимы как черт, но передают некоторую полезную информацию.

Когда GHC симпатично печатает тип с полиморфными типами, он печатает тип каждой полиморфной переменной типа после конструктора типов. С целью. Так что, если у вас было объявление вроде:

data Foo (x :: k) y (z :: k2) = Foo y

GHC будет красиво печатать тип Foo (конструктор данных) как y -> Foo k k1 x y z, Если у вас есть какое-то использование, которое определит тип одной из этих переменных типа, например..

foo :: a -> Int -> Foo a Int 5 -- Data Kind promoted Nat

Тип foo "hello" 0 будет напечатан как Foo * Nat String Int 5, Да, это ужасно Но если вы знаете, что происходит, по крайней мере, вы можете прочитать это.

'[] материал является частью DataKinds расширение. Это позволяет продвигать типы к видам, и конструкторы этого типа становятся конструкторами типов. Эти продвигаемые типы не имеют допустимых значений, даже undefined потому что их вид не совместим с *, который является видом всех типов, которые могут иметь значения с ними. Таким образом, они могут появляться только в местах, где нет такого значения. Для получения дополнительной информации см. http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/kind-polymorphism-and-promotion.html

Редактировать:

Ваш комментарий поднимает некоторые вопросы о том, как работает ghci.

-- foo.hs
{-# LANGUAGE DataKinds, PolyKinds #-}

data Foo (x :: k) y (z :: k1) = Foo y

Когда вы загружаете файл в ghci, он не активирует интерактивные расширения, которые использовались в файле.

GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :l foo
[1 of 1] Compiling Main             ( foo.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t Foo
Foo :: y -> Foo * * x y z
*Main> :set -XPolyKinds
*Main> :t Foo
Foo :: y -> Foo k k1 x y z

Так что да. PolyKinds расширение должно быть включено в ghci, чтобы оно по умолчанию использовало полиморфные виды в типе. И я попытался определить мой foo функция в файле, но она действительно вызвала эту версию GHC. Упс. Я думаю, что это сейчас исправлено, но я полагаю, было бы неплохо проверить ghc trac. В любом случае, я могу определить его в интерактивном режиме, и он отлично работает.

*Main> :set -XDataKinds
*Main> let foo :: a -> Int -> Foo a Int 5 ; foo = undefined
*Main> :t foo "hello" 0
foo "hello" 0 :: Foo * GHC.TypeLits.Nat [Char] Int 5
*Main> :m + GHC.TypeLits
*Main GHC.TypeLits> :t foo "hello" 0
foo "hello" 0 :: Foo * Nat [Char] Int 5

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

Но все работает так, как я сказал, обещаю. Я просто пропустил некоторые детали о том, где какие расширения были необходимы, в частности, оба PolyKinds а также DataKinds, Я предположил, что, поскольку вы использовали их в своем коде, вы их поняли. Вот документация на PolyKinds расширение: http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/kind-polymorphism.html

Answer 2

Это связано с неудачной реализацией в отношении печати. Виды можно рассматривать как "типы типов". Обратите внимание на следующее:

>:t []
[] :: [a]
>:k '[]
'[] :: [*]

Как [a] означает "для всех типов, [a]", [*] значит "для всех видов" *, [*] ". Однако количество рассуждений, которые вы можете сделать с типами, намного меньше, чем с типами. Например, a -> a указывает на оба as одного типа, но * -> * означает оба * может быть любого типа (это можно рассматривать как * -> * это тип a -> b "поднял" на добрый уровень). Но нет возможности поднять тип a -> a на добром уровне. Это означает, что [a] а также [*] не совсем аналогичны. [*] ближе к чему-то вроде [forall a . a], Более кратко, но менее точно, вы могли бы сказать, что нет никакого способа различить "полиморфные" виды, поскольку не существует такого понятия, как "переменные типа". (Примечание: -XPolyKinds включает то, что в документации называется "полиморфные виды", но все равно не дает истинного полиморфизма)

Поэтому, когда вы пишете HList :: [*] -> * (что на самом деле означает HList (k :: [*]) :: *) вы указываете, что тип параметра первого типа должен быть [*]и "значения", которые типа [*] может взять '[], * ': '[], * ': * ': '[], так далее.

Теперь проблема. При печати вещей, вид которых был ограничен, например, первый параметр типа HNil, он постарается включить все виды информации. По какой-то причине вместо того, чтобы писать

HNil :: HList ('[] :: '[*])
^ data         ^ type   ^ kind 

что на самом деле будет означать, что * имеет в виду вид '[], он печатает вещи в дико запутанном формате, свидетелем которого вы были. Эту информацию необходимо иметь, потому что вещи, которые "хранятся" в списке, не обязательно должны быть открытыми (это название для *). Вы могли бы иметь что-то вроде:

data Letter = A | B -- | C .. etc
data LetterProxy p 

data HList (k :: [Letter])  where
  HNil  :: HList '[]
  (:+:) :: LetterProxy (a :: Letter) -> HList t -> HList (a ': t)

что очень глупо, но все еще действует!

Я считаю, что эта неудача обусловлена ​​двумя причинами. Во-первых, если вещи были напечатаны в указанном мной формате, результат :i для определенных типов данных или классов будет очень долго и очень нечитаемым. Во-вторых, виды очень новые (только начиная с версии 7.4?), Поэтому не много времени было потрачено на то, чтобы решить, как печатать родственные вещи, потому что никто еще не уверен в том, как виды должны / будут работать.