haskell - 约束的类型别名不与上下文共享相同的变量绑定(bind)行为

Question

我一直在使用 -XConstraintKinds 来帮助缓解过于冗长的上下文，并发现变量绑定(bind)方面存在一个有趣的不一致之处:

{-# LANGUAGE
    TypeFamilies
  , ConstraintKinds
  , FlexibleContexts
  #-}

-- works
foo :: ( callTree ~ SomeTypeFunc output
       , OtherTypeFunc input ~ callTree
       ) => input -> output


type FooCtx input output =
  ( callTree ~ SomeTypeFunc output
  , OtherTypeFunc input ~ callTree
  )

-- doesn't work
foo' :: FooCtx input output =>
        input -> output

除了将 callTree 引入顶级范围之外，是否有解决方法？

Answer 1

没有真正的不一致，只是这样

1. 类型签名中的自由类型变量会自动添加 forall 量词，因此第一种情况实际上相当于

   foo :: forall callTree output input. ( callTree ~ SomeTypeFunc output
          , OtherTypeFunc input ~ callTree
          ) => input -> output
   

2. type 声明右侧的所有自由类型变量都必须是参数，不能使用任何不在范围内的变量。

这并不是特定于约束类型的，除了一个不幸的事实，即您不能将 forall 量词直接应用于约束，这意味着我不知道通用使此类约束类型声明起作用的解决方法。

在您的特定示例中，( OtherTypeFunc input ~ SomeTypeFunc output ) 应该是等效的，但我假设您确实对更复杂的示例感兴趣，在该示例中，此类重写不起作用。

我可以想到一种不同的解决方法，通过在约束右侧包含值来以不同的方式更改类型声明的参数:

{-# LANGUAGE TypeFamilies, ConstraintKinds, FlexibleContexts, RankNTypes #-}

type family OtherTypeFunc a
type family SomeTypeFunc a

type FooCtx input output value =
  forall callTree. ( callTree ~ SomeTypeFunc output
  , OtherTypeFunc input ~ callTree
  ) => value

-- This now works
foo' :: FooCtx input output ( input -> output )

foo' = undefined