我宣告了一個接受值的型別：
class NonEmpty a where
example :: a
而且，我宣告了補集類：
import Data.Void
class Empty a where
exampleless :: a -> Void
證明一個函式空間是空的很容易：
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
有沒有辦法繞過這個問題？
uj5u.com熱心網友回復：
您可以將這兩個類合并為一個表示該型別是否被居住的可判定性：
{-# 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
uj5u.com熱心網友回復：
我不認為有一個非常好的方法。標準的替代方法是使用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 ...
轉載請註明出處，本文鏈接：https://www.uj5u.com/caozuo/434786.html