如何证明函数 space 不为空？

Question

我声明了一个 class 接受值的类型：

class NonEmpty a where
    example :: a

另外，我声明了补码 class:

import Data.Void

class Empty a where
    exampleless :: a -> Void

演示一个函数space是空的很容易：

instance (NonEmpty a, Empty b) => Empty (a -> b) where
    exampleless f = exampleless (f example)

但是它的补码呢？ Haskell 不允许我同时拥有这些实例：

instance Empty a => NonEmpty (a -> b) where
    example = absurd . exampleless

instance NonEmpty b => NonEmpty (a -> b) where
    example _ = example

有什么方法可以绕过这个问题吗？

Answer 1

我认为没有什么好办法。标准的替代方法是使用 newtype 包装器来选择用户在每种情况下想要的实例。

newtype EmptyDomain a b = ED { unED :: a -> b }
newtype InhabitedCodomain a b = IC { unIC :: a -> b }

instance Empty a => NonEmpty (EmptyDomain a b) where ...
instance NonEmpty b => NonEmpty (InhabitedCodomain a b) where ...

Answer 2

您可以将这两个类合并成一个，表达 该类型是否有人居住的可判定性:

{-# LANGUAGE TypeFamilies, DataKinds
      , KindSignatures, TypeApplications, UndecidableInstances
      , ScopedTypeVariables, UnicodeSyntax #-}

import Data.Kind (Type)
import Data.Type.Bool
import Data.Void

data Inhabitedness :: Bool -> Type -> Type where
  IsEmpty :: (a -> Void) -> Inhabitedness 'False a
  IsInhabited :: a -> Inhabitedness 'True a

class KnownInhabitedness a where
  type IsInhabited a :: Bool
  inhabitedness :: Inhabitedness (IsInhabited a) a

instance ∀ a b . (KnownInhabitedness a, KnownInhabitedness b)
              => KnownInhabitedness (a -> b) where
  type IsInhabited (a -> b) = Not (IsInhabited a) || IsInhabited b
  inhabitedness = case (inhabitedness @a, inhabitedness @b) of
    (IsEmpty no_a, _) -> IsInhabited $ absurd . no_a
    (_, IsInhabited b) -> IsInhabited $ const b
    (IsInhabited a, IsEmpty no_b) -> IsEmpty $ \f -> no_b $ f a

要再次获得更简单的界面，请使用

{-# LANGUAGE ConstraintKinds #-}

type Empty a = (KnownInhabitedness a, IsInhabited a ~ 'False)
type NonEmpty a = (KnownInhabitedness a, IsInhabited a ~ 'True)

exampleless :: ∀ a . Empty a => a -> Void
exampleless = case inhabitedness @a of
   IsEmpty no_a -> no_a

example :: ∀ a . NonEmpty a => a
example = case inhabitedness @a of
   IsInhabited a -> a

如何证明函数 space 不为空？

How can I demonstrate that a function space is not empty?

haskell

is-empty