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?
CodePudding user response:
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 ...
CodePudding user response:
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