9

次のデータ型と型クラス（適切な言語拡張子を持つ）があると想像してください。

data Zero=Zero
data Succ n = Succ n
class Countable t where
      count :: t -> Int
instance Countable Zero where
      count Zero = 0

instance (Countable n) => Countable (Succ n) where
      count (Succ n) = 1 + count n

整数から、適切な型クラスインスタンスのインスタンスを私に与える関数を書くことは可能でしょうか？基本的にはf、count (f n) = n

私の試みは次のようなものでしたが、これによりコンパイル時にいくつかのタイプエラーが発生します。

f::(Countable k)=> Int -> k
f 0 = Zero
f n = Succ $ f (n-1)

解決策を探しているときに依存型に関する議論に何度も遭遇しましたが、それらの議論を自分のユースケースにマッピングすることはまだできていません。

コンテキスト：これにより、「なぜこれを実行したいのか」というタイプの質問がたくさん発生することを理解しているためです。

私は現在Data.HList、異種リストを操作するためにパッケージを使用しています。shuffleこのライブラリでは、整数を指定すると、リストnのth要素を最後にシフトする関数を作成したいと思います。n

たとえば、もし持っていたら、与えl=1:"Hello":32:500たいと思います。shuffle 1 l1:32:500:"Hello"

私はshuffle0次のユースケースに答える特殊な関数を書くことができましたshuffle 0：

shuffle0 ::(HAppend rest (HCons fst HNil) l')=>HCons fst rest -> l'
shuffle0 (HCons fst rest) = hAppend rest (HCons fst HNil)

nextまた、次のように、関数を「ラップ」するこの関数を作成しましたnext (shuffle n) = shuffle (n+1)。

next :: (forall l l'. l -> l') -> (forall e l l'.(HCons e l) -> (HCons e l'))
next f = \(HCons e l)-> HCons e  $ (f l)

型署名が役に立たないように感じます。つまり、長さのエンコードがありません（問題が発生する可能性があります）。

shuffle 0=shuffle0
shuffle n= next (shuffle (n-1))

GHCは、シャッフルのタイプを推測できないことに不満を持っています。

タイプはおそらく十分に確立されていないので、これは私を本当に驚かせません。

直感的には、リストの長さについて言及する必要があると思います。type関数を使用して特定のHListタイプの長さを取得できます。HLengthいくつかの適切に選択された制約を使用して、シャッフルを書き直し、サウンドになります（少なくとも私は思います）。

問題は、選択した長さのタイプレベルのバージョンを取得して、呼び出しで使用できるようにする必要があることです。これでうまくいくかどうかさえわかりませんが、もっとチャンスがあると思います。

4

1 に答える 1

6

あなたの最初の質問に答えるために、完全な従属型システム（Has​​kellにはない）なしでは、整数の型レベルの帰納的表現にそのようなffromを書くことはできません。Intただし、「コンテキスト」で説明する問題は、Haskellでそのような関数を必要としません。

以下はおおよそあなたが探しているものだと思います：

 {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, FunctionalDependencies, UndecidableInstances #-}

 import Data.HList

 data Z = Z
 data S n = S n

 class Nat t
 instance Nat Z
 instance Nat n => Nat (S n)

 class (Nat n, HList l, HList l') => Shuffle n l l' | n l -> l' where
     shuffle :: n -> l -> l'

 instance Shuffle Z HNil HNil where
     shuffle Z HNil = HNil

 instance (HAppend xs (HCons x HNil) ys, HList xs, HList ys) => Shuffle Z (HCons x xs) ys where
     shuffle Z (HCons x xs) = hAppend xs (HCons x HNil)

 instance (Shuffle n xs ys) => Shuffle (S n) (HCons x xs) (HCons x ys) where
     shuffle (S n) (HCons x xs) = HCons x (shuffle n xs)

例えば

 *Main> shuffle (S Z) (HCons 1 (HCons "Hello" (HCons 32 (HCons 500 HNil))))
 HCons 1 (HCons 32 (HCons 500 (HCons "Hello" HNil)))

この定義の背後にある一般的な手法は、最初に非依存型バージョンを作成する方法（たとえば、ここでは、要素をリストの最後にシャッフルする方法）を考え、次にこれを型レベル（制約）に変換することです。バージョン。shuffleの再帰的構造は、型クラスインスタンスの制約の再帰的構造によって正確に反映されていることに注意してください。

これはあなたがやろうとしていることを解決しますか？

于 2013-01-30T10:08:39.603 に答える