9

環境

SI プレフィックスを表す Haskell モジュールを作成しています。

module Unit.SI.Prefix where

各 SI プレフィックスには、対応するデータ型があります。

data Kilo = Kilo deriving Show
data Mega = Mega deriving Show
data Giga = Giga deriving Show
data Tera = Tera deriving Show

-- remaining prefixes omitted for brevity

問題

2 つの SI プレフィックスを適用すると、2 つのプレフィックスのどちらが小さいかを静的に判断する関数を書きたいと思います。例えば：

-- should compile:
test1 = let Kilo = smaller Kilo Giga in ()
test2 = let Kilo = smaller Giga Kilo in ()

-- should fail to compile:
test3 = let Giga = smaller Kilo Giga in ()
test4 = let Giga = smaller Giga Kilo in ()

初期解

型クラスと機能依存関係を一緒に使用するソリューションを次に示します。

{-# LANGUAGE FunctionalDependencies #-}                                                                                         
{-# LANGUAGE MultiParamTypeClasses #-}

class Smaller a b c | a b -> c where smaller :: a -> b -> c

instance Smaller Kilo Kilo Kilo where smaller Kilo Kilo = Kilo
instance Smaller Kilo Mega Kilo where smaller Kilo Mega = Kilo
instance Smaller Kilo Giga Kilo where smaller Kilo Giga = Kilo
instance Smaller Kilo Tera Kilo where smaller Kilo Tera = Kilo

instance Smaller Mega Kilo Kilo where smaller Mega Kilo = Kilo
instance Smaller Mega Mega Mega where smaller Mega Mega = Mega
instance Smaller Mega Giga Mega where smaller Mega Giga = Mega
instance Smaller Mega Tera Mega where smaller Mega Tera = Mega

instance Smaller Giga Kilo Kilo where smaller Giga Kilo = Kilo
instance Smaller Giga Mega Mega where smaller Giga Mega = Mega
instance Smaller Giga Giga Giga where smaller Giga Giga = Giga
instance Smaller Giga Tera Giga where smaller Giga Tera = Giga

instance Smaller Tera Kilo Kilo where smaller Tera Kilo = Kilo
instance Smaller Tera Mega Mega where smaller Tera Mega = Mega
instance Smaller Tera Giga Giga where smaller Tera Giga = Giga
instance Smaller Tera Tera Tera where smaller Tera Tera = Tera

上記の解決策は問題を正しく解決しているように見えますが、欠点があります。型クラスのインスタンスの数は、型の数に対して2 次です。

質問

おそらく対称性を利用して、型クラスインスタンスの数を型の数に対して線形に減らす方法はありますか?

ここでは Template Haskell を使用する方が適切かもしれません。その場合は、解決策として遠慮なく提案してください。

ありがとう！

4

2 に答える 2

7

このような場合は、TH の方が適していると言えます。とはいえ、とにかく型でやります。

ここでの問題は、すべてが離散的すぎることです。接頭辞を反復して正しいものを見つけることはできず、必要な順序付けの推移性を表現していません。どちらのルートでも解決できます。

再帰的なソリューションの場合、最初に型レベルで自然数とブール値を作成します。

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}

data No = No deriving (Show)
data Yes = Yes deriving (Show)

newtype S nat = Succ nat deriving (Show)
data Z = Zero deriving (Show)

type Zero  = Z
type One   = S Zero
type Two   = S One
type Three = S Two

簡単な算術演算:

type family Plus x y :: *
type instance Plus x Z = x
type instance Plus Z y = y
type instance Plus (S x) (S y) = S (S (Plus x y))

type family Times x y :: *
type instance Times x Z = Z
type instance Times x (S y) = Plus x (Times y x)

「以下」述語と単純な条件関数:

type family IsLTE n m :: *
type instance IsLTE Z Z = Yes
type instance IsLTE (S m) Z = No
type instance IsLTE Z (S n) = Yes
type instance IsLTE (S m) (S n) = IsLTE m n

type family IfThenElse b t e :: *
type instance IfThenElse Yes t e = t
type instance IfThenElse No t e = e

そして、SI接頭辞からそれらが表すマグニチュードへの変換:

type family Magnitude si :: *
type instance Magnitude Kilo = Three
type instance Magnitude Mega = Three `Times` Two
type instance Magnitude Giga = Three `Times` Three

...等。

小さいプレフィックスを見つけるには、次のようにします。

type family Smaller x y :: *
type instance Smaller x y = IfThenElse (Magnitude x `IsLTE` Magnitude y) x y

ここにあるものはすべて、型とそれに存在する単一の nullary コンストラクターの間に 1 対 1 の対応があることを考えると、これは次のようなジェネリック クラスを使用して用語レベルに変換できます。

class TermProxy t where term :: t
instance TermProxy No where term = No
instance TermProxy Yes where term = Yes
{- More instances here... -}

smaller :: (TermProxy a, TermProxy b) => a -> b -> Smaller a b
smaller _ _ = term

必要に応じて詳細を入力します。

もう 1 つのアプローチは、機能的な依存関係と重複するインスタンスを使用して、ギャップを埋めるジェネリック インスタンスを作成することです。そのため、キロ < メガ、メガ < ギガなどの特定のインスタンスを作成し、これがキロ < ギガも意味することを推測させることができます。 .

これは、関数の依存関係を原始的な論理プログラミング言語として扱うことに深く入り込みます。Prolog を使用したことがある場合は、大まかなアイデアが得られるはずです。より宣言的なアプローチに基づいてコンパイラーに物事を理解させることができるので、これはある意味では良いことです。一方で、それはちょっとひどいので...

  • インスタンスは、制約を確認せずに選択され、インスタンス ヘッドのみが選択されます。
  • 解決策を探すための後戻りはありません。
  • この種のものを表現するにはUndecidableInstances、GHC が終了することを知っているものに関する非常に保守的な規則のために、有効にする必要があります。ただし、型チェッカーを無限ループに陥らせないように注意する必要があります。たとえば、次のような例Smaller Kilo Kilo Kiloや次のような例が与えられた場合、偶然にそれを行うのは非常に簡単です-(Smaller a s c, Smaller t b s) => Smaller a b c理由を考えてください。

Fundeps と重複するインスタンスは、厳密には型ファミリよりも強力ですが、全体的に使いにくく、後者が使用するより機能的で再帰的なスタイルと比較すると、やや場違いに感じられます。

ああ、完全を期すために、ここに 3 番目のアプローチがあります。今回は、自然数に変換して構造的再帰を使用するのではなく、再帰的なソリューションを直接実装するためにインスタンスの重複によって得られる余分な力を悪用しています。

まず、必要な順序を型レベルのリストとして具体化します。

data MIN = MIN deriving (Show)
data MAX = MAX deriving (Show)

infixr 0 :<
data a :< b = a :< b deriving (Show)

siPrefixOrd :: MIN :< Kilo :< Mega :< Giga :< Tera :< MAX
siPrefixOrd = MIN :< Kilo :< Mega :< Giga :< Tera :< MAX

いくつかの重複するシェナニガンを使用して、 types に等値述語を実装します。

class (TypeEq' () x y b) => TypeEq x y b where typeEq :: x -> y -> b
instance (TypeEq' () x y b) => TypeEq x y b where typeEq _ _ = term

class (TermProxy b) => TypeEq' q x y b | q x y -> b
instance (b ~ Yes) => TypeEq' () x x b 
instance (b ~ No) => TypeEq' q x y b

代替の「未満」クラスには、次の 2 つの簡単なケースがあります。

class IsLTE a b o r | a b o -> r where
    isLTE :: a -> b -> o -> r

instance (IsLTE a b o r) => IsLTE a b (MIN :< o) r where
    isLTE a b (_ :< o) = isLTE a b o

instance (No ~ r) => IsLTE a b MAX r where
    isLTE _ _ MAX = No

次に、型レベルのブール値のケース分析に基づいて再帰ステップを延期するために使用される補助クラスを使用した再帰ケース:

instance ( TypeEq a x isA, TypeEq b x isB
         , IsLTE' a b isA isB o r
         ) => IsLTE a b (x :< o) r where
    isLTE a b (x :< o) = isLTE' a b (typeEq a x) (typeEq b x) o

class IsLTE' a b isA isB xs r | a b isA isB xs -> r where
    isLTE' :: a -> b -> isA -> isB -> xs -> r

instance (Yes ~ r) => IsLTE' a b Yes Yes xs r where isLTE' a b _ _ _ = Yes
instance (Yes ~ r) => IsLTE' a b Yes No xs r where isLTE' a b _ _ _ = Yes
instance (No ~ r) => IsLTE' a b No Yes xs r where isLTE' a b _ _ _ = No
instance (IsLTE a b xs r) => IsLTE' a b No No xs r where
    isLTE' a b _ _ xs = isLTE a b xs

本質的に、これは型レベルのリストと 2 つの任意の型を取り、リストをYesたどり、最初の型が見つかったNo場合、または 2 番目の型が見つかった場合、またはリストの最後にヒットした場合に戻ります。

これは実際には一種のバグであり (一方または両方のタイプがリストにない場合に何が起こるかを考えれば理由がわかります)、失敗する傾向があります。このような直接再帰は、GHC のコンテキスト削減スタックを使用します。非常に浅いので、それを使い果たして、あなたが望む答えではなく、タイプレベルのスタックオーバーフローを取得するのは簡単です (ハハ、はい、ジョークはそれ自体を書き込みます)。

于 2011-08-26T16:49:49.887 に答える
3

タイプをタイプレベルの自然数にマッピングし、それらを使用して比較を行うことができます。対応する番号にマッピングする型ごとに 1 つのインスタンスを指定するだけでよいため、線形になるはずです。

Haskell Wikiの型演算のページには、型レベルの自然数を扱う良い例がいくつかあります。始めるには良い場所です。

また、同様の方法で SI 単位を操作するための、Hackage 上の人気のあるパッケージ Dimension が既に存在することにも注意してください。これが彼らのコードでどのように実装されているかを見てみる価値があるかもしれません。

于 2011-08-26T16:42:55.520 に答える