種類リストはどのくらい正確に機能しますか？

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 

そこからIその'[]は'[] *の糖であり、(':) * x yのx ': yである。それは何ですか？リスト要素の種類ですか？とにかく、そのようなリストはどういうものですか？それは言語に組み込まれたものですか？

Answer 1

これは*です...残念です。これは、GHCの多色データ型用のきれいなプリンタの結果です。それは、文法的に無効なものになるが、いくつかの有用な情報を伝える。

GHCが多型を持つ型を綺麗に出力する場合、型コンストラクタの後に各多型変数の種類を出力します。順番に。だから、あなたのような宣言があった場合：y -> Foo k k1 x y zとしてFooのタイプ（データコンストラクタを）かなり-印刷し

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

GHCを。あなたはややこれらのタイプ変数の1つのようなものを釘付けにいくつかの使用を持っていた場合、...

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 

[OK]を、よく、私はそれが修飾されていないNatを表示するためにインポートが必要だった忘れてしまいました。そして、タイプ印刷だけを実演していたので、私は実装について気にしなかったので、undefinedは十分です。

しかし、すべてはになると私は約束しました。私は何の拡張機能が必要なのか、特にPolyKindsとDataKindsの両方について、いくつかの詳細を省きました。あなたのコードでそれらを使用していたので、あなたはそれらを理解していたと私は推測しました。 PolyKinds拡張に関するドキュメントは次のとおりです。http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/kind-polymorphism.html

Answer 2

これは、印刷に関する不幸な実装によるものです。種類は「種類の種類」と考えることができます。次の点に注意してください。ただ、 "すべてのタイプのため、[a]" [a]手段、[*]手段のような

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

"すべて種類*ため、[*]"。しかし、あなたが種類で行うことができる推論の量は、型よりもはるかに小さいです。例えば、a -> aは、両方ともaが同じタイプであることを示しますが、* -> *は、両方とも*がいずれのタイプであってもよいことを意味します（* -> *はa -> bが種類レベルに「持ち上げられました」と考えることができます）。しかし種類a -> aを種類レベルに上げる方法はありません。つまり、[a]と[*]はあまりよく似ていません。 [*]は[forall a . a]のようなものに近いです。より簡潔ではありますが、あまり正確ではないが、「多型」の種類を区別するための方法は存在しないと言うことができます。あなたが（本当にHList (k :: [*]) :: *を意味する）HList :: [*] -> *を書くとき、あなたが示しているので、

：（サイドノートでは​​は、どのようなドキュメント・コール「多型の種類」を可能にし、それはまだあなたの真の多型を与えるものではありません）その最初の種類今

問題など、タイプパラメータは[*]であるべき、と種類[*]の種類を取ることができる「値は、」'[]、* ': '[]、* ': * ': '[]です。タイプが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) 

これは非常にばかだが、まだ有効です！

この誤植は、2つの理由によるものだと私は信じています。第一に、私が述べた形式で物が印刷された場合、特定のデータタイプまたはクラスのための:iの結果は非常に長く、非常に判読不能になります。第二に、種類は非常に新しく（わずか7.4歳前後）、親切なものを印刷する方法を決めるのに多くの時間は費やされていません。