有没有办法在声音响起时将 foralls 推过构造函数？答案

【问题标题】：Is there a way to push foralls past constructors when sound?有没有办法在声音响起时将 foralls 推过构造函数？
【发布时间】：2017-07-07 01:36:29
【问题描述】：

假设我有

data Foo p =
    NoFoo
  | YesFoo (forall a. p a)

我会写

fromFoo :: Foo p -> Maybe (p a)
fromFoo NoFoo = Nothing
fromFoo (YesFoo p) = Just p

也可以换一种方式：

toFoo :: forall p.
         (forall a. Maybe (p a))
      -> Foo p
toFoo m =
  case m :: Maybe (p ()) of
    Nothing -> NoFoo
    Just _ -> YesFoo (fromJust m)

fromJust 太恶心了！ toFoo 实际上是完全的，因为参数化确保 m @a 的行为与 m @() 完全相同，但这很糟糕。有没有更干净的方法？

编辑：rampion 指出这可以写得更简洁，仍然使用fromJust。我只是意识到它可以做得有点幽默，取笑新手：

toFoo m
  | isNothing m = NoFoo
  | otherwise = YesFoo (fromJust m)

我认为避免创建应用 fromJust 的唯一方法是变得超级邪恶：

toFoo Nothing = NoFoo
toFoo (Just x) = YesFoo (unsafeCoerce# x)

【问题讨论】：

作为记录，我猜你没有使用签名toFoo :: forall p. (Maybe (forall a. p a)) -> Foo p（这会使实现变得微不足道），因为“GHC 还不支持暗示性多态性”错误消息。
@rampion，啊，现在我明白你的问题了。我认为这是一个有效的问题，但可能略有不同。
@rampion 这个问题不等于(forall a. Maybe (p a)) -> Maybe (forall a. p a)吗？不是您评论中的类型
实际上，是的：newtype Pred a = Pred { runPred :: a -> Bool }。 forall a. Pred a 是一个适用于任何a 的多态谓词，但Pred (forall a. a)（我们暂时假设这是一个有效类型）是一个单态谓词，仅适用于多态值。所以没有像这样推动foralls 的通用方法。您将获得的任何答案都必须针对Maybe（或至少其界面的某些部分，例如Functor）。
啊，当然。急切地想看看这个问题是否能得到答案！

标签： haskell

【解决方案1】：

到目前为止我能想到的最好的仍然是fromJust，但它更简单：

toFoo :: forall p.
         (forall a. Maybe (p a))
      -> Foo p
toFoo Nothing = NoFoo
toFoo m = YesFoo $ fromJust m

【讨论】：

另一个令人作呕的选择是匹配Just 构造函数，然后匹配unsafeCoerce 其内容进行泛化。