类型运算符的顺序和类型要求

Question

玩弄 TypeOperators 我已经尝试实现 $ 和 . 这样我就可以去掉我的程序中的任何括号（没有冒犯任何漂亮的 Lispers）。在这样做的过程中，我同构地复制了定义。首先，我只尝试使用 $，因为你不需要 . 的强大功能。

{-# LANGUAGE TypeOperators #-}
type f $ a = f a

f :: Int -> IO $ Either String Int
f n = undefined

太棒了。这编译，我很满足。

{-# LANGUAGE TypeOperators #-}
type f $ a = f a

f :: Int -> IO $ Maybe $ Either String Int
f n = undefined

这应该行得通吧？

TyCo.hs:4:18:
    Expecting one more argument to ‘Maybe’
    The second argument of ‘$’ should have kind ‘*’,
      but ‘Maybe’ has kind ‘* -> *’
    In the type signature for ‘f’:
      f :: Int -> (IO $ Maybe) $ Either String Int

显然不是。

{-# LANGUAGE TypeOperators #-}
type f $ a = f a
type (f * g) a = f (g a)

f :: Int -> IO * Maybe $ Either String Int
f n = undefined

抱着盲目的希望，我试试

TyCo.hs:5:6:
    Type synonym ‘*’ should have 3 arguments, but has been given 2
    In the type signature for ‘f’:
      f :: Int -> (IO * Maybe) $ Either String In

在我无知的昏迷中，我提出了一个问题：WHY这行不通吗？

Answer 1

第一个问题与$的固定性有关，您可以通过注意括号所在的位置来查看错误消息中的标志。 (IO $ Maybe) 是部分应用的类型同义词，导致错误。您不能部分应用类型同义词，因为它需要比较它们，这相当于比较函数。

LiberalTypeSynonyms 只是让 GHC 在进行类型检查之前解包类型同义词，即 (IO * Maybe) $ Either String Int 变成 (IO (Maybe (Either String Int))) 然后然后它类型检查。这意味着 * 不再部分应用，程序编译。

类型运算符的顺序和类型要求

Sequence of type-operators and kind requirements

haskell

types

type-level-computation