haskell - () 作为空约束

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

()有 kind*或Constraint，根据上下文，从不a -> Constraint。同样(,)有 kind* -> * -> *或Constraint -> Constraint -> Constraint，取决于上下文。

—西蒙·佩顿-琼斯

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

class Empty x
instance Empty x

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

Answer 2

Jon Purdy 的回答是正确的。如果您想要一件事，无论数量如何（实例头部或类型系列 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

Answer 3

()有 kindConstraint并不意味着应用于 a Type。

Answer 4

这些都可以正常工作，具体取决于您想要什么：

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