How do good lists work?

Question

I recently read vinyl that uses weird types of list types. After reading a little about types and vinyl, I understood their intuitive understanding, and I was able to crack it together.

 {-# 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 gives

 data HList $a where HNil :: HList ('[] *) (:+:) :: a -> (HList t) -> HList ((':) * at) -- 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 ((':) * at)) -- 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 ((':) * at)) -- Defined at /tmp/test.hs:29:10 *Main> :i HList data HList $a where HNil :: HList ('[] *) (:+:) :: a -> (HList t) -> HList ((':) * at) -- 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 ((':) * at)) -- 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 ((':) * at)) -- Defined at /tmp/test.hs:29:10 

From which I understand that '[] is sugar for '[] * and x ': y for (':) * xy . What does it do? Is this a list item? Also, what is such a list? Is this something built into the language?

Answer 1

This * is ... Unhappy. This is the result of the large GHC multikin data type printer. This leads to syntactically invalid words, but it conveys some useful information.

When the GHC nicely prints a type with polymorphic views, it prints the type of each variable of the polymorphic type after the type constructor. OK. Therefore, if you have an ad like:

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

GHC will print the type Foo (data constructor) as y -> Foo k k1 xyz . If you had any use that pinned a little to one of these type variables, for example ..

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

Type foo "hello" 0 will print as Foo * Nat String Int 5 . Yes, that’s terrible. But if you know what is happening, at least you can read it.

The material '[] is part of the DataKinds extension. This allows you to advertise types by type, and constructors of this type become type constructors. These advanced types do not have valid values, not even undefined , because their type is not compatible with * , which is the type of all types that can have values ​​with them. Therefore, they can appear only in those places where there is no such value. For more information see http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/kind-polymorphism-and-promotion.html

Edit:

Your comment brings up some points about how ghci works.

 -- foo.hs {-# LANGUAGE DataKinds, PolyKinds #-} data Foo (x :: k) y (z :: k1) = Foo y 

When you upload a file to ghci, it does not activate the interactive extensions that were used in the file.

 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 * * xyz *Main> :set -XPolyKinds *Main> :t Foo Foo :: y -> Foo k k1 xyz 

So yes. The PolyKinds must be included in ghci so that it defaults to polymorphic types in the type. And I tried to define my Foo function in a file, but it really ruined this version of ghc. Oops I think it is fixed now, but I believe that checking ghc trac would be nice. In any case, I can define it interactively and it works great.

 *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 

Ok, I forgot that import was needed to display Nat unqualified. And since I was just demonstrating typography, I didn't care about the implementation, so undefined is good enough.

But everything works, as I said, I promise. I just did not talk about what extensions are needed, in particular, both PolyKinds and DataKinds . I assumed that since you used them in your code, you understood them. Here's the documentation for the PolyKinds extension: http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/kind-polymorphism.html

Answer 2

This is due to some unsuccessful implementation regarding printing. Views can be considered as "types of types." Please note the following:

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

Just as [a] means "for all types of a, [a] ", [*] means "for all types * , [*] ". However, the number of considerations you can make with views is much less than with types. For example, a -> a indicates that both a are the same type, but * -> * means that both * can be of any type (it can be represented as * -> * - this is the type a -> b , " raised "by level view). But there is no way to raise type a -> a to level level. This means that [a] and [*] not exactly the same. [*] closer to something like [forall a . a] [forall a . a] . More concisely, but less accurately, you could say that there is no way to distinguish between "polymorphic" species, since there is no such thing as "species variables". (side note: -XPolyKinds allows documentation to call "polymorphic types", but it still doesn't give you true polymorphism)

So, when you write HList :: [*] -> * (which really means HList (k :: [*]) :: * ), you indicate that the type of the first type parameter must be [*] , and "values" that can have types of type [*] are '[] , * ': '[] , * ': * ': '[] , etc.

Now the problem. When printing objects that were limited, like the parameter of the first type of HNil , it will try to include all the type information. For some reason, instead of writing

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

which actually indicates that * is of type '[] , it prints things in the wildly confusing format you saw. You must have this information because the kind of thing "stored" inside the list does not have to be open (this is the name for * ). You might have something like:

 data Letter = A | B -- | C .. etc data LetterProxy p data HList (k :: [Letter]) where HNil :: HList '[] (:+:) :: LetterProxy (a :: Letter) -> HList t -> HList (a ': t) 

which is extremely stupid but still valid!

I believe that this failure is due to two reasons. Firstly, if something was printed in the format that I stated, the result :i for certain data types or classes will be very long and very unreadable. Secondly, the views are very new (only around with 7.4?), Therefore, not so much time has been spent on deciding how to print good things, because no one is yet sure which species should / will work.