СУХАЯ аннотация типа для свойств QuickCheck - PullRequest
0 голосов
/ 03 октября 2018

С помощью QuickCheck можно написать параметрически полиморфные свойства, например:

associativityLaw :: (Eq a, Show a, Semigroup a) => a -> a -> a -> Property
associativityLaw x y z = (x <> y) <> z === x <> (y <> z)

Это всего лишь пример, поскольку мои действительные свойства более сложны, но они достаточно хорошо иллюстрируют проблему.Это свойство проверяет, что для типа a оператор <> является ассоциативным.

Представьте, что я хотел бы использовать это свойство для нескольких типов.Я мог бы определить свой список тестов следующим образом:

tests =
  [
    testGroup "Monoid laws" [
      testProperty "Associativity law, [Int]" (associativityLaw :: [Int] -> [Int] -> [Int] -> Property),
      testProperty "Associativity law, Sum Int" (associativityLaw :: Sum Int -> Sum Int -> Sum Int -> Property)
    ]
  ]

Это работает, но кажется излишне многословным.Я хотел бы иметь возможность просто заявить, что для данного свойства a должно быть [Int], или a должно быть Sum Int.

Примерно так: гипотетический синтаксис:

testProperty "Associativity law, [Int]" (associativityLaw :: a = [Int]),
testProperty "Associativity law, Sum Int" (associativityLaw :: a = Sum Int)

Есть ли способ сделать это, возможно, с расширением языка GHC?

Моя настоящая проблема связана с типами с более высоким родом, и я хотел бы иметь возможностьчтобы сказать, что, например, f a это [Int], или f a это Maybe String.

Мне известно этот ответ , но оба варианта (Proxy и Tagged) кажется, как описано там, по крайней мере, слишком неловко, чтобы действительно решить проблему.

1 Ответ

0 голосов
/ 03 октября 2018

Вы можете использовать TypeApplications для привязки переменных типа следующим образом:

{-# LANGUAGE TypeApplications #-}

associativityLaw @[Int]

В том случае, если вы упомянули, что у вас тип с большим родом, и вы хотите связать f a с [Int],Вы должны связать переменные типа f и a отдельно:

fmap @[] @Int

Для функций с более чем одной переменной типа можно применять аргументы в следующем порядке:

f :: a -> b -> Int

-- bind both type vars    
f @Int @String

-- bind just the first type var, and let GHC infer the second one
f @Int

-- bind just the second type var, and let GHC infer the first one
f @_ @String

Иногда «порядок» переменных типа может быть неочевидным, но вы можете использовать :type +v и запросить GHCi для получения дополнительной информации:

λ> :t +v traverse
traverse
  :: Traversable t =>
     forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b)

В стандартном haskell «порядок» переменных типане имеет значения, так что GHC просто делает это для вас.Но при наличии TypeApplications порядок имеет значение :

map :: forall b a. (a -> b) -> ([a] -> [b])
-- is not the same as
map :: forall a b. (a -> b) -> ([a] -> [b])

По этой причине, когда вы работаете с высокопараметрическим кодом, или вы ожидаете, что ваши пользователи захотятиспользуйте TypeApplications в своих функциях, вы можете явно установить порядок переменных типа вместо того, чтобы позволить GHC определять порядок для вас, с помощью ExplicitForAll:

{-# LANGUAGE ExplicitForAll #-}

map :: forall a b. (a -> b) -> ([a] -> [b])

, что очень похоже на <T1, T2> в Java или C #

...