2

Show のような制約を受け取り、RHS をShow のインスタンスではない型に制約する型関数を返す型関数を作成することは可能ですか?

署名は次のようなものになります

type family Invert (c :: * -> Constraint) :: * -> Constraint
4

2 に答える 2

10

いいえ。これを行うことは決して許可されていないというのは、言語の設計原則です。ルールは、プログラムが有効である場合、さらにinstances を追加してもプログラムが壊れてはならないというものです。これがオープンワールドの仮定です。あなたの望む制約はかなり直接的な違反です:

data A = A
f :: Invert Show a => a -> [a]
f x = [x]
test :: [A]
test = f A

動作しますが、追加します

instance Show A

それを壊します。したがって、元のプログラムは最初から有効であってはならず、したがってInvert存在することはできません。

于 2019-08-05T06:18:00.923 に答える
3

HTNW が答えたように、一般に、型がクラスのインスタンスではないと主張することはできないと考えられています。ただし、特定のクラスのインスタンスを持つことが決して可能ではないことを具象型に対してアサートすることは確かに可能です。アドホックな方法は次のとおりです。

{-# LANGUAGE ConstraintKinds, KindSignatures, AllowAmbiguousTypes
           , MultiParamTypeClasses, FlexibleInstances #-}

import GHC.Exts (Constraint)

class Non (c :: * -> Constraint) (t :: *) where
  nonAbsurd :: c t => r

しかし、これは安全ではありません – インスタンスを書く唯一の方法は、

instance Non Show (String->Bool) where
  nonAbsurd = undefined

しかし、その後、他の誰かが偽物を思いつき、月がグリーンチーズでできていることを証明するinstance Show (String->Bool)ためにあなたを使用することができます.nonAbsurd

インスタンスを不可能にするためのより良いオプションは、それを「ブロック」することです。そのインスタンスを自分で「プリエンプティブに」記述しますが、実際に呼び出すのは型エラーになるようにします。

import Data.Constraint.Trivial -- from trivial-constraint

instance Impossible0 => Show (String->Bool) where
  show = nope

誰かがそのインスタンスを追加しようとしたり、使用しようとすると、明確なコンパイラ エラーが発生します。

于 2019-08-05T11:03:43.890 に答える