You are viewing beroal

язык, на котором не говорят - map, filter, catMaybes [entries|archive|friends|userinfo]
beroal

[ website | personal website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

map, filter, catMaybes [Oct. 14th, 2013|01:00 am]
Previous Entry Add to Memories Share Next Entry
[Tags|, , ]

∃a. ∃b. ∃m:a->Maybe b. ∀f:a->b. ∀p:a->Bool. ¬(catMaybes . map m == map f . filter p)

Другими словами, не всякий catMaybes можно выразить через map и filter. Ситуация такая же, как с инъекциями и сюръекциями. Для каждой инъекции s:A->B, кроме случая, когда A пустое и B населённое, существует сюръекция r такая, что r∘s=id. Это «кроме» портит всё удовольствие.

Значит, придётся отказаться от filter в пользу функции zyu

zyu m = catMaybes . map m
zyu (m1 <=< m0) == zyu m1 . zyu m0

где <=< — композиция в категории Клейсли над Maybe.
LinkReply

Comments:
[User Picture]From: thedeemon
2013-10-14 02:47 am (UTC)

(Link)

> ∃m:a->Maybe b. ∀f:a->b. ∀p:a->Bool. ¬(catMaybes . map m == map f . filter p)

А можно посмотреть на терм такого типа? Конструктивное доказательство, то бишь.
[User Picture]From: migmit
2013-10-14 12:46 pm (UTC)

(Link)

Если тип b пуст, а m = const Nothing, то всё так и есть. Поскольку никаких f:a->b нету, там и проверять нечего.
[User Picture]From: beroal
2013-10-14 12:50 pm (UTC)

(Link)

Ну, писать формальное доказательство не входило в мои планы. Рассмотрите случай, когда a населённое, b пустое, m = const Nothing. Тогда ∀f:a->b. … истинное.
[User Picture]From: thedeemon
2013-10-14 02:30 pm (UTC)

(Link)

А не надо ли тогда перед формулой ∃b поставить, раз речь не про любой b?
[User Picture]From: beroal
2013-10-14 02:36 pm (UTC)

(Link)

надо :-)
From: (Anonymous)
2013-10-14 02:09 pm (UTC)

(Link)

module CatMaybes where

open import Relation.Binary.Core using (_≢_)
open import Function using (_∘_)
open import Data.Unit using (⊤)
open import Data.Empty using (⊥)
open import Data.Bool using (Bool; true; false)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.List using (List; []; _∷_; map; filter; fromMaybe; concat)
open import Data.Product using (Σ; _,_)

th : Σ Set (λ A → Σ Set (λ B → Σ (A → Maybe B) (λ m →
       (f : A → B)
     → (p : A → Bool)
     → concat ∘ map fromMaybe ∘ map m ≢ map f ∘ filter p)))
th = ⊤ , (⊥ , ((λ _ → nothing) , (λ f _ _ → f record { })))