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

user_4540658 0
Viewed 140

I declared a class of types that admits a value:

class NonEmpty a where
    example :: a

And also, I declared the complement class:

import Data.Void

class Empty a where
    exampleless :: a -> Void

Demonstrating a function space is empty is easy:

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

But what about its complement? Haskell doesn't let me have these instances simultaneously:

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

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

Is there any way to bypass this problem?

is-empty haskell
2 Answers

You can merge the two classes together into one that expresses decidability of whether or not the type is inhabited:

{-# 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

To get again your simpler interface, use

{-# 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
user_7459030

I don't think there's a really great way. The standard alternative is to use newtype wrappers to choose which instance the user wants in each case.

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 ...
user_7916040
Related