4

ちょっとした楽しみとして、どれくらいの長さかわかる Type レベルのリストを作成したいと思いました。このようなもの：

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

import GHC.TypeLits

data family TypeList a (n::Nat)

data instance TypeList a (0) = EmptyList
data instance TypeList a (1) = TL1 a (TypeList a (0))
data instance TypeList a (2) = TL2 a (TypeList a (1))
data instance TypeList a (3) = TL3 a (TypeList a (2))

しかし、もちろん、これを次のように一般化したいと思います。

data instance TypeList a (n)   = TL3 a (TypeList a (n-1))

しかし、これはエラーを生成します:

    TypeList.hs:15:53: parse error on input `-'
    Failed, modules loaded: none.

別の試み:

data instance TypeList a (n+1) = TL3 a (TypeList a (n))

また、エラーが生成されます。

    Illegal type synonym family application in instance: n + 1
    In the data instance declaration for `TypeList'

このようなことが可能でなければならないと思います。次の表記法を使用することは間違いなく可能です。

data Zero
data Succ a

しかし、見栄えの良いバージョンではわかりません。

4

2 に答える 2

6

型レベルのNat改善は GHC 7.8 で行われ、これが可能になりました!

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

import GHC.TypeLits

data family List (n :: Nat) a
data instance List 0 a = Nil
data instance List n a = a ::: List (n - 1) a

infixr 8 :::

usingは、自分で作成するようなデータ構造Listと同じくらい自然です。[]

λ. :t 'a' ::: 'b' ::: 'c' ::: Nil
'a' ::: 'b' ::: 'c' ::: Nil :: List 3 Char
于 2014-04-03T01:12:33.267 に答える
3

GHC 7.6 のように、型レベルの Nats ではこのようなことはできません。0 :: Nat名前が示唆するものにもかかわらず、現在、型との間に多かれ少なかれ関係はありません(たとえば、便利なことを行うことができるあなたのand と1 :: Natは異なります)。これは、GHC の将来のバージョンで改善される予定です。ZeroSucc Zero

于 2012-12-16T04:40:46.053 に答える