6

私は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

4

2 に答える 2

7

それ*は... 残念です。これは、ポリカインド データ型に対する GHC の pretty-printer の結果です。構文的に無効な結果になりますが、いくつかの有用な情報を伝えます。

GHC が多相カインドを持つ型をきれいに出力するとき、型コンストラクタの後に各多相型変数のカインドを出力します。順番に。したがって、次のような宣言があるとします。

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

FooGHC は(データ コンストラクター)の型を としてきれいに出力し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

于 2013-11-26T22:08:49.847 に答える
0

これは、印刷に関するいくつかの残念な実装によるものです。カインドは「タイプのタイプ」と考えることができます。次の点に注意してください。

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

同様に、「[a]すべての種類の a、[a]」を[*]意味し、「すべての種類 *の、 」を意味し[*]ます。ただし、種類で実行できる推論の量は、型よりもはるかに少なくなります。たとえば、a -> aは両方aの が同じ型であることを示しますが、どちらも任意の型になる可能性があること* -> *を意味します (種類レベルに「持ち上げられた」型*と考えることができます)。しかし、タイプを種類レベルに上げる方法はありません。これは、とがまったく類似していないことを意味します。のようなものに近いです。より簡潔に言えば、正確性は劣​​りますが、「種類変数」のようなものは存在しないため、「多態的」種類を区別する方法はないと言えます。（サイドノート：* -> *a -> ba -> 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)

これは非常にばかげていますが、それでも有効です。

私は、この誤機能には 2 つの理由があると考えています。まず、私が述べた形式で出力した:i場合、特定のデータ型またはクラスの結果は非常に長くなり、非常に読みにくくなります。第二に、カインドは非常に新しい (7.4 以降?) ため、カインドされたものを印刷する方法を決定するのに多くの時間が費やされていません。

于 2013-11-27T00:26:12.437 に答える