2

無限の一連のアクションがあり、それぞれが特定の型の結果を返すとしましょう。何かのようなもの：

newtype Stream a = Stream (IO (a, Stream a))

しかし、a時間の経過とともに変化します。このシーケンスを強く型付けしたい。次のような任意の無限型シーケンスと単純なアプローチには明らかに意味がありません。

data HStream :: [u] -> * where Cons :: Proxy x -> HStream xs -> HStream (x ': xs)

infiniteInt = Cons (Proxy :: Proxy Int) infiniteInt

Haskell の型システムではサポートされていない無限型になります。しかし、最終的に周期的な HLists (つまり、ある時点からどのような型シーケンスが繰り返されるかなど) に問題はないと思います: [Bool, Int, Int, Sting, Int, Sting, Int, Sting ... ])。また、無限型を記述するための強力な正規化方法や、有限数のステップでチェックできる無限型の等価性の証拠を提供する方法があれば、そのような無限型を含むプログラムを型チェックできるはずです。

そのような型をHaskellでどのように表現して使用できるか、誰にもわかりませんか? 今のところ、無限の最終的に周期的な hlist から始めましょう。ただし、より広いクラスの無限の tupes に対して一般化する方法と、一般化の制限がどこにあるのかについて誰かが考えを持っている場合にも感謝します。

4

2 に答える 2

1

一般的なオプションの 1 つはHList、すべての要素の型をエンコードする から、有効なパスに沿った遷移のみを保証する型整列リスト (または、より一般的には型整列シーケンス) に切り替えることです。

data TAList c x z where
  Nil :: TAList c x x
  Cons :: c x y -> TAList c y z -> TAList c x z

そのため、慎重に遷移をエンコードすることができcます。無限の型整列リストは、最終的な型引数で多態的であるため、問題ありません。xz

Atkey の代わりに McBride スタイルのインデックス スキームを使用して、複雑さを犠牲にして柔軟性を高めることもできます。

于 2016-05-05T01:23:37.227 に答える