Подтвердить что ты не робот

Можно ли аннотировать функцию специальных свойств (например, сюръективность)?

Скажем, у меня есть функция более высокого порядка f :: (a -> b) -> (a -> b). Но f ведет себя корректно, только если функция ввода сюръективна. В любом случае, чтобы это произошло в Хаскелле? Например, я действительно хочу, чтобы подпись типа f была чем-то вроде:

f :: (Surjective (a -> b)) => (a -> b) -> (a -> b)

Но это не работает, потому что я не хочу, чтобы все функции типа a -> b были объявлены сюръективными, только некоторые из них. Например, возможно, f преобразует сюръективную функцию в неъективную функцию.

Мы могли бы обернуть функции в специальный тип данных data Surjective f = Surjective f и определить

f :: Surjective (a -> b) -> (a -> b)

но это затруднит назначение нескольких свойств функции.

Есть ли удобный способ сделать это на практике? Возможно ли это в теории?

4b9b3361

ОТВЕТЫ

Ответ 1

Это пример того, как сюръективность может быть выражена в Agda:

module Surjectivity where

open import Data.Product using ( ∃; ,_ )
open import Relation.Binary.PropositionalEquality using ( _≡_; refl )

Surjective : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _
Surjective {A = A} {B = B} f = ∀ (y : B) → ∃ λ (x : A) → f x ≡ y

Например, id является сюръективным (простое доказательство):

open import Function using ( id )

id-is-surjective : ∀ {a} {A : Set a} → Surjective {A = A} id
id-is-surjective _ = , refl

Взятие другой тождественной функции, которая работает только для сюръективных функций:

id-for-surjective : ∀ {a b} {A : Set a} {B : Set b} → (F : A → B) → {proof : Surjective F} → A → B
id-for-surjective f = f

мы можем передать id до id-for-surjective's с его доказательством сюръективности в качестве свидетеля:

id′ : ∀ {a} {A : Set a} → A → A
id′ = id-for-surjective id {proof = id-is-surjective}

так что id′ является той же функцией, что и id:

id≡id′ : ∀ {a} {A : Set a} → id {A = A} ≡ id′
id≡id′ = refl

Попытка передать не-сюръективную функцию на id-for-surjective's была бы невозможна:

open import Data.Nat using ( ℕ )

f : ℕ → ℕ
f x = 1

f′ : ℕ → ℕ
f′ = id-for-surjective f {proof = {!!}} -- (y : ℕ) → ∃ (λ x → f x ≡ y) (unprovable)

Аналогично, многие другие свойства могут быть выражены таким образом, стандартная библиотека Agda уже имеет необходимые определения (например, Function.Surjection, Function.Injection, Function.Bijection и другие модули).

Ответ 2

Сначала вы обычно используете объявление newtype, а не объявление data. GHC использует newtypes для проверки типов, но затем эффективно стирает их во время компиляции, поэтому сгенерированный код более эффективен.

Использование newtype для такого вида аннотации является общим решением в Haskell, хотя, как вы указываете, оно не полностью удовлетворяет, если вам нужно обернуть многие свойства вокруг значения.

Вы можете объединить newtype с типами классов. Объявите экземпляр типа класса для класса Surjective для любой оболочки newtype, которую вы хотите, и сопоставьте с этим типом класса в таких функциях, как f, вместо того, чтобы требовать конкретную оболочку newtype.

Еще приятнее, конечно, будет возможность заставить компилятор проверить, действительно ли функция сюръективна... но это скорее открытая исследовательская проблема.: -)

Ответ 3

Мы можем подобрать зависимые типы simlutate в 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.)

Набор 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)) ..