1

TypeNats に関する GHC wikiのセクションを閲覧していたときに、この非常に興味深い例を見つけました。彼らはタイプのリストを作成しています:

type family Get (n :: Nat1) (xs :: [*]) :: *
type instance Get Zero     (x `: xs) = x
type instance Get (Succ n) (x `: xs) = Get n xs

これについてもっと知りたいです。この機能は 7.6.1 では実装されていないと思います (少なくとも私にはコンパイルされません)。何を探すべきか考えていますか？

4

1 に答える 1

5

このコードは GHC 7.6 でほぼ問題なく動作します -- いくつかの拡張機能をオンにし、` の代わりに ' を使用する必要があります (どうやら構文が変更されたようです?)。この例は以下をコンパイルします。

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

data Nat1 = Zero | Succ Nat1

type family Get (n :: Nat1) (xs :: [*]) :: *
type instance Get Zero     (x ': xs) = x
type instance Get (Succ n) (x ': xs) = Get n xs

これらの TypeNats ではなく、型のリストだけに関心がある場合は、次のような例がより便利になることがあります。

data HList :: [*] -> * where
  HNil :: List '[]
  HCons :: t -> List ts -> List (t ': ts)

ここで説明したように。最も関連性の高い GHC 拡張機能はDataKindsであり、最も関連性の高い論文はおそらくGiving Haskell a Promotionです。

于 2013-01-24T06:29:39.613 に答える