2

漠然としたタイトルで申し訳ありません。ここにいくつかのコンテキストがあります：http://themonadreader.files.wordpress.com/2013/08/issue221.pdf

前号の GADTs の記事では、Nat 型と、さまざまな型レベルのリスト関数 (concat、!!、head、repeat など) で使用する NatSing 型を紹介しています。これらの関数のいくつかでは、Nat 型で + と < を定義するための型ファミリを作成する必要があります。

data Nat = Zero | Succ Nat

data NatSing (n :: Nat) where
    ZeroSing :: NatSing Zero
    SuccSing :: NatSing n -> NatSing (Succ n)

data List (n :: Nat) a where
    Nil  :: List n a
    Cons :: a -> List n a -> List (Succ n) a

とにかく、呼び出し元の便宜のために、通常[a]を に変換する関数「リスト」を作成しました。これには、 （リンクされた記事から）のList n aように、入力としてリストの長さが必要です。repeat

list :: [a] -> NatSing n -> List n a
list []      ZeroSing    = Nil
list (x:xs) (SuccSing n) = Cons x (list xs n)
list _       _           = error "length mismatch"

ヘルパー関数を利用するとよいtoNatSing :: Int -> NatSing nので、上記は次のように記述できます。

list :: [a] -> List n a
list xs = list' xs (toNatSing $ length xs)
  where
    list' :: [a] -> NatSing n -> List n a
    list' = ... -- same as before, but this time I simply "know" the function is no longer partial

そのような関数を書くことは可能toNatSingですか? 私は型と格闘してきましたが、まだ何も思いつきません。

どうもありがとう！

4

3 に答える 3

6

いいえ、そのような関数を書くことはできません。

タイプの関数

Int -> NatSing n

は、任意の整数をポリモーフィック に変換できると言いNatSingます。しかし、ポリモーフィックはありませんNatSing。

ここで望んでいるように見えるのはn、着信によって決定されたことIntです。それは依存型になります：

(n :: Int) -> NatSing n

Haskell ではそのようなことはできません。Agda または Idris または別の依存型言語を使用する必要があります。シングルトンを使ったハックは、これを回避するまさに Haskell の方法です。値に基づいて区別したい場合は、値をタイプ レベルに引き上げる必要がありますNatSing。

存在型でラップすることにより、 NatSingfor some を返す関数を書くことができます:nn

data ExNatSing where
  ExNatSing :: NatSing n -> ExNatSing

しかし、これは実際にはあまりメリットがありません。まとめるnと、それに関するすべての情報が失われ、後でそれに基づいて決定を下すことができなくなります。

まったく同じ引数で、関数を定義することも期待できません

list :: [a] -> List n a

入力作業を節約するために使用できる唯一の方法は、NatSing値を自動的に構築する型クラスを定義することです。

class CNatSing (n :: Nat) where
  natSing :: NatSing n

instance CNatSing Zero where
  natSing = ZeroSing

instance CNatSing n => CNatSing (Succ n) where
  natSing = SuccSing natSing

次に、次のように言えます。

list :: CNatSing n => [a] -> List n a
list xs = list' xs natSing
  where
    list' :: [a] -> NatSing n -> List n a
    list' = ... -- same as before, but still partial

ここで、 this を使用する型コンテキストにより、GHC は right を埋めますNatSing。ただし、関数の呼び出し元はこれを使用する場所を選択できるため、この関数はまだn部分的です。[Int]長さ3を a として使用したい場合List (Succ Zero) Int、クラッシュします。

繰り返しますが、代わりにこれを実存的なものにまとめることができます:

data SomeList a where
  SomeList :: NatSing n -> List n a -> SomeList a

それからあなたは書くことができます

list :: [a] -> SomeList a
list []       = SomeList ZeroSing Nil
list (x : xs) = case list xs of
                  SomeList n xs -> SomeList (SuccSing n) (x : xs')

繰り返しになりますが、利点は小さいですが、 とは対照的にExNatSing、少なくとも 1 つがあります。一時的に a をラップ解除して、SomeLista で動作する関数に渡すことができList n a、これらによってリストの長さがどのように変換されるかについて型システムの保証を得ることができます。機能。

于 2013-11-06T00:05:01.660 に答える
1

Louis Wassermann が言ったように、あなたが望むものに最も近いのはNatSing、外側からモノモーフィックにする実存的なラッパーです。

ただし、基本的には長さの型チェックを破棄するだけで、標準的な整数型が残されるため、これはかなり役に立たないと思います。それにはもっと簡単な方法があります。たとえば、ばかげた標準整数型と通常の Haskell リストを使用することです...

しかし、おそらくそれほど役に立たない代替手段が 1 つあります。x関数から何らかの値を返す場合、または代わりに高次を渡して;で呼び出す場合は、ほとんど同等であることを覚えておいてください xLisp は、このような継続渡しのトリックが特に好きだと思います。

あなたの例では、任意の長さタイプのリストを受け入れることができる関数が必要です。そうですね、そのような関数は確かに存在します。たとえば、同じ長さの 2 つのリストを必要とするスカラー積ですが、長さは気にしません。そして、単純な単形数を返します。sum簡単にするために、リストタイプをさらに単純に考えてみましょう。

sumSing :: Num a => List (n::Nat) a -> a
sumSing Nil = 0
sumSing (Cons x ls) = x + sumSing ls

次に、次のことができます。

{-# LANGUAGE RankNTypes     #-}

onList :: (forall n . CNatSing n => List n a -> b) -> [a] -> b
f`onList`l = f (list l)

（クラス制約listのあるkosmicusのバリアントであること）そしてそれを次のように呼び出しますCNatSing

sumSing `onList` [1,2,3]

...もちろん、それ自体は実存的解決策よりも有用ではありません（実際には、このようなものに脱糖すると思いますRankN）。しかし、スカラー積の例のように、ここでさらに多くのことを行うことができます。2 つのリストを提供し、実際に型システムを通じてそれらが同じ長さであることを保証します。これは実在論でははるかに醜いでしょう: 基本的に別のTwoEqualLenLists型が必要です。

于 2013-11-06T00:43:47.137 に答える