() 作为空约束

Question

如何表示空约束？

对于以下文件

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}

import Data.Kind(Type, Constraint)

type Empty = (() :: Type -> Constraint)

main :: IO ()
main = return ()

ghc 8.2.2 答案

constraint.hs:6:15: error:
    • Expected kind ‘* -> Constraint’, but ‘()’ has kind ‘*’
    • In the type ‘(() :: Type -> Constraint)’
      In the type declaration for ‘Empty’
  |
6 | type Empty = (() :: Type -> Constraint)
  |

我想念什么？

我知道以下解决方案

{-# LANGUAGE FlexibleInstances #-}

class Empty x
instance Empty x

但我想知道为什么 () 不起作用

Answer 1

() 具有种类 Constraint，并不意味着应用于 Type.

Answer 2

() has kind * or Constraint, depending on context, never a -> Constraint. Similarly (,) has kind * -> * -> * or Constraint -> Constraint -> Constraint, depending on context.

— Simon Peyton-Jones

只是()只是重载了无论是类型还是约束。也就是说，你会写 () => a，而不是 (() a) => a。所以我认为：

class Empty x
instance Empty x

这里是正确的解决方案。（也许类似的东西应该在 base 中。）

Answer 3

根据您的需要，这些都可以正常工作：

type Empty = (() :: Constraint)
type ConstEmpty x = (() :: Constraint)

Answer 4

是正确的。如果你想要一件事你可以不管 arity（实例头或类型族 LHS 除外），你将需要使用一些样板：

{-# language PolyKinds, ConstraintKinds, FlexibleInstances,
    MultiParamTypeClasses, TypeFamilies #-}

import Data.Kind (Constraint)

class Unit1 a
instance Unit1 a
class Unit2 a b
instance Unit2 a b
...

type family Unit :: k
type instance Unit = (() :: Constraint)
type instance Unit = Unit1
type instance Unit = Unit2
...

然后

Prelude K> type Empty = (Unit :: Type -> Constraint)
Prelude K> :kind! Empty
Empty :: * -> Constraint
= Unit1

() 作为空约束

() as empty constraint

haskell

constraint-kinds