假设我有一个高阶函数f :: (a -> b) -> (a -> b)。但f只有在输入函数是满射的情况下才能正常运行。无论如何，有没有强制这种情况发生在 Haskell 中？例如，我真的希望f's 类型签名是这样的：
f :: (Surjective (a -> b)) => (a -> b) -> (a -> b)
但这不起作用，因为我不希望该类型的所有函数都a -> b被声明为满射，只有其中一些函数。例如，可能f将一个满射函数转换为一个非满射函数。
我们可以将函数包装在一种特殊的数据类型data Surjective f = Surjective f中，并定义
f :: Surjective (a -> b) -> (a -> b)
但这会使为一个函数分配多个属性变得困难。
在实践中有没有方便的方法来做到这一点？这在理论上是可能的吗？
如果类型依赖于由其类型唯一确定的值，我们可以在 Haskell 中模拟依赖类型。当然，这不是依赖类型，但有时它可能很有用。
因此，让我们在类型级别构建一种小型建设性集合论。每种类型将代表一个特定的功能，并将由一个值（不包括所有底部的东西）占据。
将 F 定义为满足以下条件的最小集合：
id:: a -> a位于 F。term:: a -> ()位于 F。init:: Empty -> a在 F 中（其中 Empty 表示空集）。p1 :: (a,b) -> a位于 F。i1 :: a -> Either a b位于 F。flip :: (a,b) -> (b,a)位于 F。f::a -> b都g::b -> c在 F 中，则g.f :: a -> c在 F 中。f::a -> b都g::c -> d在 F 中，则以下函数在 F 中：
f*g :: (a,c) -> (b,d)
f*g (x,y) = (f x,g y)
f + g :: Either a b -> Either c d
(f+g) (Left x) = f x
(f+g) (Right y) = g y`
集合 F 旨在表示在 Haskell 中类型级别可编码的函数，同时其各种属性如超射性、单射性等可由 Haskell 中的类型级别函数证明。
借助关联类型，我们可以将 F 编码干净，如下所示：
class Function f where
type Dom f :: *
type Codom f :: *
apply :: f -> Dom f -> Codom f
data ID a = ID -- represents id :: a -> a
instance Function (ID a) where
type Dom (ID a) = a
type Codom (ID a) = a
apply _ x = x
data P1 a b = P1 -- represents the projection (a,b) -> a
instance Function (P1 a b) where
type Dom (P1 a b) = (a,b)
type Codom (P1 a b) = a
apply _ (x,y) = x
...
data f :.: g = f :.: g -- represents the composition (f.g)
instance ( Function f
, Function g
, Dom f ~ Codom g)
=> Function (f :.: g) where
type Dom (f :.: g) = Dom g
type Codom (f :.: g) = Codom f
apply (f :.: g) x = apply f (apply g x)
...
类型级谓词“f 是满射的”可以表示为类实例：
class Surjective f where
instance Surjective (ID a) where
instance Surjective (P1 a b) where
instance (Surjective f,Surjective g)
=> Surjection (f :.: g) where
..
最后，可以定义采用那些可证明的满射函数的高阶函数：
surjTrans :: (Function fun,Surjective fun)
=> fun -> Dom fun -> Codom fun
surjTrans surj x = apply surj x
对于注入、同构等也是类似的。例如，可以声明仅将（构造）同构作为参数的高阶函数：
isoTrans :: (Function fun,Surjective fun,Injective fun)
=> fun -> Dom fun -> Codom fun
isoTrans iso x = apply iso x
如果转换采用更有趣的形式，那么它必须是一个类方法，并由每个函数的结构递归定义（由其类型唯一确定）。
我当然不是逻辑或 Haskell 方面的专家，我真的很想知道这个理论有多么强大。如果你发现了这个，你能发布一个更新吗？
这是完整的代码：
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
infixl 6 :.:
infixl 5 :*:
infixl 4 :+:
data TRUE
data Empty
class Function f where
type Dom f :: *
type Codom f :: *
apply :: f -> Dom f -> Codom f
instance Function (a -> b) where
type Dom (a->b) = a
type Codom (a->b) = b
apply f x = f x
data ID a = ID
data Initial a = Initial
data Terminal a = Terminal
data P1 a b = P1
data P2 a b = P2
data I1 a b = I1
data I2 a b = I2
data FLIP a b = FLIP
data COFLIP a b = COFLIP
data f :.: g = f :.: g
data f :*: g = f :*: g
data f :+: g = f :+: g
instance Function (ID a) where
type Dom (ID a) = a
type Codom (ID a) = a
apply _ x = x
instance Function (Initial a) where
type Dom (Initial a) = Empty
type Codom (Initial a) = a
apply _ _ = undefined
instance Function (Terminal a) where
type Dom (Terminal a) = a
type Codom (Terminal a) = ()
apply _ _ = ()
instance Function (P1 a b) where
type Dom (P1 a b) = (a,b)
type Codom (P1 a b) = a
apply _ (x,y) = x
instance Function (P2 a b) where
type Dom (P2 a b) = (a,b)
type Codom (P2 a b) = b
apply _ (x,y) = y
instance Function (I1 a b) where
type Dom (I1 a b) = a
type Codom (I1 a b) = Either a b
apply _ x = Left x
instance Function (I2 a b) where
type Dom (I2 a b) = b
type Codom (I2 a b) = Either a b
apply _ y = Right y
instance Function (FLIP a b) where
type Dom (FLIP a b) = (a,b)
type Codom (FLIP a b) = (b,a)
apply _ (x,y) = (y,x)
instance Function (COFLIP a b) where
type Dom (COFLIP a b) = Either a b
type Codom (COFLIP a b) = Either b a
apply _ (Left x) = Right x
apply _ (Right y) = Left y
instance ( Function f
, Function g
, Dom f ~ Codom g)
=> Function (f :.: g) where
type Dom (f :.: g) = Dom g
type Codom (f :.: g) = Codom f
apply (f :.: g) x = apply f (apply g x)
instance (Function f, Function g)
=> Function (f :*: g) where
type Dom (f :*: g) = (Dom f,Dom g)
type Codom (f :*: g) = (Codom f,Codom g)
apply (f :*: g) (x,y) = (apply f x,apply g y)
instance (Function f, Function g)
=> Function (f :+: g) where
type Dom (f :+: g) = Either (Dom f) (Dom g)
type Codom (f :+: g) = Either (Codom f) (Codom g)
apply (f :+: g) (Left x) = Left (apply f x)
apply (f :+: g) (Right y) = Right (apply g y)
class Surjective f where
class Injective f where
class Isomorphism f where
instance Surjective (ID a) where
instance Surjective (Terminal a) where
instance Surjective (P1 a b) where
instance Surjective (P2 a b) where
instance Surjective (FLIP a b) where
instance Surjective (COFLIP a b) where
instance (Surjective f,Surjective g)
=> Surjective (f :.: g) where
instance (Surjective f ,Surjective g )
=> Surjective (f :*: g) where
instance (Surjective f,Surjective g )
=> Surjective (f :+: g) where
instance Injective (ID a) where
instance Injective (Initial a) where
instance Injective (I1 a b) where
instance Injective (I2 a b) where
instance Injective (FLIP a b) where
instance Injective (COFLIP a b) where
instance (Injective f,Injective g)
=> Injective (f :.: g) where
instance (Injective f ,Injective g )
=> Injective (f :*: g) where
instance (Injective f,Injective g )
=> Injective (f :+: g) where
instance (Surjective f,Injective f)
=> Isomorphism f where
surjTrans :: (Function fun,Surjective fun)
=> fun -> Dom fun -> Codom fun
surjTrans surj x = apply surj x
injTrans :: (Function fun,Injective fun)
=> fun -> Dom fun -> Codom fun
injTrans inj x = apply inj x
isoTrans :: (Function fun,Isomorphism fun)
=> fun -> Dom fun -> Codom fun
isoTrans iso x = apply iso x
g1 :: FLIP a b
g1 = FLIP
g2 :: FLIP a b :*: P1 c d
g2 = FLIP :*: P1
g3 :: FLIP a b :*: P1 c d :.: P2 e (c,d)
g3 = FLIP :*: P1 :.: P2
i1 :: I1 a b
i1 = I1
例如，以下是一些输出（查看 Haskell 在类型检查时如何“证明”这些递归属性）：
isoTrans g1 (1,2)
==> (2,1)
surjTrans g2 ((1,2),(3,4))
==> ((2,1),3)
injTrans g2 ((1,2),(3,4))
==> No instance for (Injective (P1 c0 d0)) ..
surjTrans i1 1 :: Either Int Int
==> No instance for (Surjective (I1 Int Int)) ..
injTrans i1 1 :: Either Int Int
==> Left 1
isoTrans i1 1 :: Either Int Int
==> No instance for (Surjective (I1 Int Int)) ..
首先，您通常使用newtype声明而不是data声明。GHC 使用 newtypes 进行类型检查，然后在编译期间有效地擦除它们，因此生成的代码更高效。
使用newtype这种注释是 Haskell 中的一种常见解决方案，尽管正如您所指出的，如果您需要围绕一个值包装许多属性，这并不完全令人满意。
您可以newtype与类型类结合使用。Surjective在您想要的任何包装器上为类型类声明一个类型类实例，newtype并在函数中匹配该类型类，例如f，而不需要特定的newtype包装器。
当然，更好的是让编译器检查函数是否真的是满射的……但这是一个相当开放的研究问题。:-)