Общая функция типа (forall n. Maybe (f n)) → Возможно (forall n. (F n))

Ответ 1

Я случайно получил его, просто попробовав создать значение, которое я мог бы передать в вашу функцию easyf. У меня проблемы, если вам нужно объяснение, хотя!! см. Комментарии ниже.

data A α = A Int
data B f = B (forall α . f α)

a :: forall α . A α
a = A 3

b = B a
f (B (Just -> x)) = x -- f :: B t -> Maybe (forall α. t α)
f' (B x) = Just x -- f' :: B t -> Maybe (t α)

easy :: forall f . Maybe (forall n . (f n)) -> (forall n . Maybe (f n))
easy Nothing = Nothing
easy (Just x) = Just x

easyf :: Maybe (forall n . (A n)) -> (forall n . Maybe (A n))
easyf = easy

-- just a test
g = easyf (f b)



h :: (forall α. t α) -> Maybe (forall α. t α)
h = f . B

unjust :: (forall n . (Maybe (f n))) -> (forall n . f n)
unjust (Just x) = x

hard :: forall f. (forall n . (Maybe (f n))) -> Maybe (forall n . (f n))
hard [email protected](Just _) = g (unjust xj) where
    g :: (forall n . f n) -> Maybe (forall n . (f n))
    g = h
hard Nothing = Nothing

изменить 1

вынимая мусор сверху,

mkJust :: (forall α. t α) -> Maybe (forall α. t α)
mkJust = Just

unjust :: (forall n . (Maybe (f n))) -> (forall n . f n)
unjust (Just x) = x

hard :: forall f. (forall n . (Maybe (f n))) -> Maybe (forall n . (f n))
hard [email protected](Just _) = mkJust (unjust xj)
hard Nothing = Nothing

Ответ 2

Я доказал это невозможным [err, no я did not; см. ниже] в Агда:

module Proof where

open import Data.Empty
open import Data.Maybe
open import Data.Bool
open import Data.Product

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

Type : Set₁
Type = Σ ({A : Set} {F : A → Set} → (∀ n → Maybe (F n)) → Maybe (∀ n → F n)) (λ f → ∀ {A} {F : A → Set} x y → f {F = F} x ≡ f y → (∀ i → x i ≡ y i))

helper : (b : Bool) → Maybe (T b)
helper true = just _
helper false = nothing

proof : ¬ Type
proof (f , pf) with inspect (f helper)
proof (f , pf) | just x with-≡ eq = x false
proof (f , pf) | nothing with-≡ eq with f {F = T} (λ _ → nothing) | pf helper (λ _ → nothing)
proof (f , pf) | nothing with-≡ eq | just x | q = x false
proof (f , pf) | nothing with-≡ eq | nothing | q with q eq true
proof (f , pf) | nothing with-≡ eq | nothing | q | ()

Конечно, это не идеальное решение, так как оно на другом языке, но я думаю, что оно соответствует довольно хорошо.

Я начал с определения Type как вашего желаемого типа функции, а также доказательство того, что функция является инъективной (Σ x P можно рассматривать как экзистенциальное высказывание "существует такое x, что P (x)" ). Поскольку мы говорим о инъективной функции, которая принимает функцию (haskell forall можно рассматривать как функцию уровня типа и то, как она кодируется в Agda), я использую точечное равенство (∀ i → x i ≡ y i), потому что логика Agda не позволит мне доказать, что x ≡ y напрямую.

Кроме этого, я просто опроверг этот тип, предоставив контрпример для булевых.

Изменить: мне просто пришло в голову, что тип включает функцию F из некоторого типа A в тип, поэтому мое доказательство не соответствует точно тому, что вы могли бы написать в Haskell. Я сейчас занят, но позже попытаюсь исправить это.

Изменить 2: мое доказательство неверно, потому что я не учитываю параметричность. Я могу сопоставить шаблон по логическим, но не по множеству, и я не могу доказать это в Agda. Я еще подумаю о проблеме:)

Ответ 3

Это легко понять, если вы посмотрите на все возможные вычислительные зависимости, каждое вычисляемое значение может иметь во время выполнения:

Выражение типа (forall n . Maybe (f n)) может быть оценено с помощью Nothing для одного типа и Just для другого типа. Следовательно, это функция, которая принимает тип как параметр.

hard :: (forall n . Maybe (f n)) -> Maybe (forall n . f n)
-- problem statement rewritten with computational dependencies in mind:
hard' :: (N -> Maybe (fN)) -> Maybe (N -> fN)

Результирующее значение этого типа Maybe (N -> fN) (будь то Nothing или Just) зависит от значения N (тип N).

Итак, ответ нет.

Ответ 4

Вопрос может быть сведен к следующему: можем ли мы написать функцию, которая перемещает фокусы следующим образом?

suicidal :: f (forall n. n) -> forall n. f n

В конце концов, если мы сможем это сделать, то все остальное легко с несколькими непроизводительными типами:

hard' :: Maybe (f (forall n. n)) -> Maybe (forall n. f n)
hard' Nothing = Nothing
hard' (Just x) = Just (suicidal x)

hard :: (forall n. Maybe (f n)) -> Maybe (forall n. f n)
hard x = hard' x -- instantiate 'n' at type 'forall n. n', thank goodness for impredicativity!

(Если вы хотите попробовать это в GHC, обязательно определите новый тип, например

newtype Forall f = Forall { unForall :: forall n. f n }

так как в противном случае GHC любит плавать forall перед стрелками и заворачивать вас.)

Но ответ на то, можно ли написать suicidal, ясно: нет, мы не можем! По крайней мере, не таким параметрическим над f. Решение должно выглядеть примерно так:

suicidal x = /\ n. {- ... -}

... и тогда нам придется пройти по "структуре" f, найдя "места", где были функции типа, и применив их к n, мы теперь имеем доступную. Ответ на исходный вопрос о hard оказывается одинаковым: мы можем написать hard для любого частного f, но не параметрически над всеми f.

Кстати, я не уверен, что то, что вы сказали о параметричности, совершенно верно:

По параметричности для любого фиксированного f :: *->* единственные полные обитатели (forall n . Maybe (f n)) будут принимать одну из двух форм: Nothing или Just z где z :: forall n . f n.

На самом деле, я думаю, что вы получаете то, что жители (эквивалентно наблюдаемому) являются одной из двух форм:

/\ n. Nothing
/\ n. Just z

... где z выше не является полиморфным: он имеет конкретный тип f n. (Примечание: нет скрытых forall.) То есть возможные условия последней формы зависят от f! Вот почему мы не можем параметризовать функцию по отношению к f.

edit: Кстати, если мы позволяем себе экземпляр Functor для f, то, конечно, все проще.

notSuicidal :: (forall a b. (a -> b) -> (f a -> f b)) -> f (forall n. n) -> forall n. f n
notSuicidal fmap structure = /\ n. fmap (\v -> v [n]) structure

... но это обман, не в последнюю очередь потому, что я понятия не имею, как перевести это на Haskell.; -)