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

Question

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?

Almeta

So, this is a nitpick, but... \_ -> () and absurd, the two implementations for NonEmpty (Void -> ()), are distinguishable functions in Haskell. Which behavior should it have? Any solution will have to choose one or the other, which seems unfortunate. – Disassemble

@DanielWagner I'm intrigued - in what concrete sense are \_ -> () :: Void -> () and absurd distinguishable? They certainly agree on all possible input values (since there are 0 of them), which is as far as I understand it the "moral" definition of equality of functions. Presumably you mean there's some Haskell function/expression that will behave differently depending on which of these 2 functions you use - and if so I'd be intrigued to see one because I can't see myself how to construct one. – Intransigent

@RobinZigmond Morally equal, yep (hence calling it a nitpick). You have to be immoral to notice the difference: applying each to undefined will throw an exception in one case and give you () in the other, which you can distinguish in IO. – Disassemble

@DanielWagner thanks - I see, and I should have thought of that! – Intransigent

@DanielWagner I'm not a fan of these arguments, because if we're going to be pedantic nitpicks we could as well also point out that measuring runtime differences in IO would allow us to distinguish two copies of the exact same code compiled with different optimisation settings. IOW, no laws / transformation rules could ever be formulated. – Viipuri

@Viipuri Okay, but these two implementations are actually different values in the domain (domain theory sense) of interest, right? Whereas an optimized version of a function is supposed to be the same value if the optimizer isn't buggy. That feels like a distinction worth making to me. – Disassemble

Answer 1

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

Viipuri

Answer 2

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

Disassemble