高階関数があるとしましょうf :: (a -> b) -> (a -> b)。ただしf、入力関数が全射である場合にのみ適切に動作します。Haskellでこれを強制する方法はありますか？たとえば、私は本当にfの型アノテーションを次のようにしたいと思っています。
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 -> aFにあります。term:: a -> ()Fにあります。init:: Empty -> aFにあります（ここで、Emptyは空のセットを表します）。p1 :: (a,b) -> aFにあります。i1 :: a -> Either a bFにあります。flip :: (a,b) -> (b,a)Fにあります。f::a -> bとが両方ともg::b -> cFにある場合、g.f :: a -> cはFにあります。f::a -> bとが両方ともg::c -> dFにある場合、次の関数は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)
...
タイプレベルの述語「fissurjective」は、クラスインスタンスとして表すことができます。
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は、型チェックにnewtypeを使用しますが、コンパイル中にそれらを効果的に消去するため、生成されたコードはより効率的です。
この種のアノテーションに使用newtypeすることはHaskellの一般的な解決策ですが、ご指摘のとおり、値の周りに多くのプロパティをラップする必要がある場合は完全に満足できるものではありません。
newtype型クラスと組み合わせることができます。特定のラッパーを必要とせずに、必要なラッパーSurjectiveで型クラスの型クラスインスタンスを宣言し、newtypeなどの関数でその型クラスと照合します。fnewtype
もちろん、さらに優れているのは、関数が本当に全射であることをコンパイラーにチェックさせる機能です...しかし、それはかなり未解決の研究問題です。:-)