haskell - 不能从 f x = f₁ y 推导出 f = f₁?

标签 haskell typechecking gadt unification

{-# LANGUAGE GADTs #-}

data Foo x y where
  Composition :: Foo b c -> Foo a b -> Foo a c
  FMap :: Functor f => (a->b) -> Foo (f a) (f b)

asFunction :: Foo a b -> a->b
asFunction (FMap m) = fmap m
-- asFunction (Composition (FMap m) (FMap n)) = fmap m . fmap n
asFunction (Composition m n) = asFunction m . asFunction n

这按预期工作...直到您取消注释 asFunction 的第二个子句!这实际上只是其他两种模式已经匹配的特殊情况的内联版本,所以我希望它没问题。但是( ghc-7.6.2ghc-7.4.1 )
Could not deduce (f ~ f1)
from the context (b1 ~ f a1, b ~ f b2, Functor f)
  bound by a pattern with constructor
             FMap :: forall (f :: * -> *) a b.
                     Functor f =>
                     (a -> b) -> Foo (f a) (f b),
           in an equation for \`asFunction'
  ...

为什么会发生这种情况,为什么不在其他条款中?在更复杂的应用程序中究竟应该做些什么来防止这种麻烦?

最佳答案

这可能与为了支持更灵活(“不饱和”)类型函数而暂时从 GHC 的类型推断系统中删除的强制左/右分解特征有关,然后是 reintroduced when it was found to have annoying effects like this .

关于haskell - 不能从 f x = f₁ y 推导出 f = f₁?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/23229210/

相关文章:

scala - 示例使用 scalaz.Lens 的 modf、modp 和 xmap

parsing - Haskell:如何使用 attoparsec 从 ByteString 读取嵌套列表

haskell - 使用 `no-code` 标志时 ghc 不报告非详尽模式匹配

haskell - 不在范围内 : type constructor or class ‘∼’

haskell - 是否有类型对齐序列的应用类比?

haskell - 在 Haskell 中定义数据结构的建议

reflection - Haskell:为什么要进行类型检查?

typescript - 如果创建库,我应该手动验证 TypeScript 中的参数吗?

ocaml - ocaml中GADT的异构列表

haskell - 为什么这个 eta 扩展是必要的?