类型约束的存在量化

Question

我不确定为什么ko不进行类型检查.有没有特别启发性的解释？

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NoMonomorphismRestriction, FlexibleInstances #-}

module Wrap where

class ExpSYM repr where
    lit :: Int -> repr

newtype Wrapped = Wrapped{unWrap :: forall repr. ExpSYM repr => repr}

a = (lit <$> Just 5) :: ExpSYM expr => Maybe expr

ko :: Maybe Wrapped
ko = do v <- a
        return $ Wrapped $ v

ok :: Maybe Wrapped
ok = do v <- Just 5
        let e = lit v
        return $ Wrapped $ e

编译器提到

SO.hs:15:14: error:
    • No instance for (ExpSYM a0) arising from a use of ‘a’
    • In a stmt of a 'do' block: v <- a
      In the expression:
        do { v <- a;
             return $ Wrapped $ v }
      In an equation for ‘ko’:
          ko
            = do { v <- a;
                   return $ Wrapped $ v }

SO.hs:16:28: error:
    • Couldn't match expected type ‘repr’ with actual type ‘a0’
        because type variable ‘repr’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a type expected by the context:
          ExpSYM repr => repr
        at SO.hs:16:18-28
    • In the second argument of ‘($)’, namely ‘v’
      In the second argument of ‘($)’, namely ‘Wrapped $ v’
      In a stmt of a 'do' block: return $ Wrapped $ v
    • Relevant bindings include v :: a0 (bound at SO.hs:15:9)
Failed, modules loaded: none.

编辑: 在Oleg的注释中找到了一个很好的解决方案来绕过这个,这是专门化类型,以便类型应用程序删除多态,添加实例

instance ExpSYM Wrapped where
   lit x = Wrapped $ lit x

然后我们有

notko :: Maybe Wrapped
notko = do v <- a    
           return $ v -- note the difference. what's the type of a ?

-- and we get all the usual goodies, no silly impredicative error
alsoOk = lit <$> Just 5 :: Maybe Wrapped

Answer 1

ko只有在那种类型的a情况下才会起作用

a :: Maybe (? expr . ExpSYM expr => expr)
a = lit <$> Just 5

...因为只有这样你才能做 - 解开它以获得多态值v :: ? expr . ExpSYM expr => expr.该值必须是多态的,因此它实际上可以用于Wrapped.

但这Maybe (? expr . ExpSYM expr => expr)是一种不可预测的类型.GHC Haskell不支持impredicative类型.

OTOH,在ok,v只是一个无聊的老整数一个引人注意的到来Just 5 :: Maybe Int.只e引入了多态性,但在Maybemonad 之外也是如此.