Ищете элегантный способ объединить монады и списки - PullRequest
Новая
       10

Ищете элегантный способ объединить монады и списки

0 голосов
/ 07 ноября 2019

Рассмотрим следующую сигнатуру модуля: 

module Test {a b} (A : Set a) (B : Set b) where

Это позволяет определять следующие функциональные типы: 

τ₁ : Set _
τ₁ = A → B → Maybe B

τ₂ : Set _
τ₂ = List A → B → Maybe B

Я хотел бы написать элегантную функцию, которая преобразуетэлемент f типа τ₁ элементу g типа τ₂. Я хочу, чтобы g был расширением f в том смысле, что он будет применяться f для каждого элемента в списке, который принимается в качестве параметра g. Моей первой попыткой было следующее: 

factor₁ : τ₁ → τ₂
factor₁ _ [] b = return b
factor₁ f (x ∷ l) b = f x b >>= factor₁ f l

Это несколько элегантно в том смысле, что для объединения вызовов функций используется, возможно, монада. Но, написав этот фрагмент кода, я почувствовал, что эта функция уже должна существовать как мета-функция где-то в стандартной библиотеке, но я не нашел такой функции. Я даже искал функции в файле списка, которые привели ко второй попытке использования foldr (это можно сделать и с помощью foldl): 

factor₂ : τ₁ → τ₂
factor₂ f l b = foldr (λ x → maybe (f x) nothing) (just b) l

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

τ₁' : Set _
τ₁' = A → Maybe B → Maybe B

τ₂' : Set _
τ₂' = List A → Maybe B → Maybe B

Функция будет очень простой и элегантной: 

factor₃ : τ₁' → τ₂'
factor₃ f = flip (foldr f)

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

У меня следующий вопрос:

  • Существует ли такая функция в стандартной библиотеке?
  • Если нет, был бы более элегантный способ написать ее?

Кроме того, вот заголовок моего модуля для того, чтобы этот пример был автономным: 

open import Data.List
open import Data.Maybe
open import Data.Maybe.Categorical
open import Category.Monad
open import Function

module Test {a b} (A : Set a) (B : Set b) where

open RawMonad {f = b} monad

РЕДАКТИРОВАТЬ: я нашел новый способ записифактор-функция, которая соответствует моим требованиям: 

factor : τ₁ → τ₂
factor f l b = foldl (λ x → (x >>=_) ∘ f) (return b) l

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

...