如何在没有模棱两可的类型错误的情况下编写此模式同义词? [英] How can I write this pattern synonym without ambiguous type errors?

问题描述

使用ViewPatterns和Data.Typeable，我设法编写了一个函数，该函数使我可以编写类似于类型的案例分析的内容.观察:

Using ViewPatterns and Data.Typeable, I’ve managed to write a function that allows me to write something resembling case analysis on types. Observe:

{-# LANGUAGE GADTs, PatternSynonyms, RankNTypes, ScopedTypeVariables
           , TypeApplications, TypeOperators, ViewPatterns #-}

import Data.Typeable

viewEqT :: forall b a. (Typeable a, Typeable b) => a -> Maybe ((a :~: b), b)
viewEqT x = case eqT @a @b of
  Just Refl -> Just (Refl, x)
  Nothing -> Nothing

evilId :: Typeable a => a -> a
evilId (viewEqT @Int -> Just (Refl, n)) = n + 1
evilId (viewEqT @String -> Just (Refl, str)) = reverse str
evilId x = x

上面的evilId函数确实非常邪恶，因为它使用Typeable完全颠覆了参数性:

The above evilId function is very evil, indeed, since it uses Typeable to completely subvert parametricity:

ghci> evilId True
True
ghci> evilId "hello"
"olleh"

由于我喜欢邪恶，对此我感到非常满意，但是上面的语法非常嘈杂.我希望能够更清楚地编写相同的代码，所以我决定写一个模式同义词:

Since I love being evil, I am very pleased with this, but the above syntax is very noisy. I would love to be able to write the same code more clearly, so I decided to write a pattern synonym:

pattern EqT :: forall b a. (Typeable a, Typeable b) => (a ~ b) => b -> a
pattern EqT x <- (viewEqT @b -> Just (Refl, x))

我认为我可以使用这种模式同义词来使我的邪恶案例分析更容易阅读:

I figured that I would be able to use this pattern synonym to make my evil case analysis much easier to read:

evilId :: Typeable a => a -> a
evilId (EqT (n :: Int)) = n + 1
evilId (EqT (str :: String)) = reverse str
evilId x = x

遗憾的是，这根本不起作用. GHC似乎在对模式进行类型检查之前未咨询我的类型注释，因此它认为b在每个模式中都是一个模棱两可的变量.有什么方法可以用模式同义词来干净地包装这些模式，还是会停留在较长的视图模式上?

Sadly, this does not work at all. GHC does not seem to consult my type annotations before typechecking the pattern, so it believes b is an ambiguous variable in each pattern. Is there any way I can cleanly wrap these patterns with a pattern synonym, or will I be stuck with my longer view patterns?

推荐答案

如果目标是找到一些简单的语法来实现您的evilId函数，则可以这样编写:

If the goal is to find some clean syntax to implement your evilId function, you can write it like this:

{-# Language ScopedTypeVariables, GADTs, TypeApplications #-}

module Demo where

import Data.Typeable

evilId :: forall a. Typeable a => a -> a
evilId x
  | Just Refl <- eqT @a @Int    = x+1
  | Just Refl <- eqT @a @String = reverse x
  | otherwise                   = x

不幸的是，这并不能解决模式同义词周围的歧义.

This doesn't help with the ambiguities surrounding your pattern synonyms, unfortunately.

这篇关于如何在没有模棱两可的类型错误的情况下编写此模式同义词?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！