4

最初の試み

この質問を簡潔にするのは難しいですが、最小限の例を提供するために、私がこのタイプを持っていると仮定します。

{-# LANGUAGE GADTs #-}
data Val where
  Val :: Eq a => a -> Val

このタイプを使用すると、次の異種のリストを作成できます。

l = [Val 5, Val True, Val "Hello!"]

しかし、残念ながら、インスタンスを書き留めると、問題が発生しEqます。

instance Eq Val where
  (Val x) == (Val y) = x == y -- type error

ああ、だから私たちはCould not deduce (a1 ~ a)。まったく正しい。定義には何も書かれておらず、同じタイプxでなければなりません。y実際、要点は、それらが異なる可能性を許容することでした。

2回目の試行

Data.Typeableミックスに取り入れて、同じタイプの場合にのみ2つを比較してみましょう。

data Val2 where
  Val2 :: (Eq a, Typeable a) => a -> Val2

instance Eq Val2 where
  (Val2 x) == (Val2 y) = fromMaybe False $ (==) x <$> cast y

これはかなりいいです。xとyが同じタイプの場合、基になるEqインスタンスを使用します。それらが異なる場合は、を返しますFalse。ただし、このチェックは実行時まで遅延されるため、nonsense = Val2 True == Val2 "Hello"文句なしにタイプチェックできます。

質問

私はここで依存型をいちゃつくことに気づきましたが、Haskell型システムが実行時に返送nonsenseするようなものを許可しながら、上記のようなものを静的に拒否することは可能ですか？sensible = Val2 True == Val2 FalseFalse

この問題に取り組むほど、必要な操作を型レベルの関数として実装するために、 HListの手法のいくつかを採用する必要があるようです。しかし、私は実存主義とGADTを使用するのは比較的新しいので、これらだけで解決策が見つかるかどうか知りたいです。したがって、答えが「いいえ」の場合は、この問題がこれらの機能の限界に達する正確な場所についての議論と、適切な手法、HListなどへの微調整に感謝します。

4

2 に答える 2

14

含まれている型に基づいて型チェックの決定を行うには、含まれている型を型パラメーターとして公開することにより、含まれている型を「記憶」する必要があります。

data Val a where
  Val :: Eq a => a -> Val a

現在Val Int、Val Boolは異なるタイプであるため、同じタイプの比較のみが許可されるように簡単に強制できます。

instance Eq (Val a) where
  (Val x) == (Val y) = x == y

ただし、Val IntとVal Boolは異なるタイプであるため、含まれているタイプを再び「忘れる」追加のレイヤーがないと、リストにそれらを混在させることはできません。

data AnyVal where
  AnyVal :: Val a -> AnyVal

-- For convenience
val :: Eq a => a -> AnyVal
val = AnyVal . Val

今、私たちは書くことができます

[val 5, val True, val "Hello!"] :: [AnyVal]

含まれている型を同時に「忘れる」と「覚える」の両方が必要になるため、単一のデータ型で両方の要件を満たすことはできないことは、今では明らかになっているはずです。

于 2011-09-27T02:38:46.310 に答える
7

したがって、異種型を使用できるコンストラクターが必要ですが、コンパイル時に認識できる異種型間の比較は拒否されます。のように：

Val True == Val "bar"  --> type error

allSame [] = True
allSame (x:xs) = all (== x) xs

allSame [Val True, Val "bar"]  --> False

しかし確かに：

(x == y) = allSame [x,y]

したがって、これらの制約を満たす関数は、型システムのいくつかの望ましいプロパティに違反すると確信しています。あなたにはそのように見えませんか？「いや、そんなことはできない」と強く思います。

于 2011-09-27T02:39:54.470 に答える