Немного пропатчил ghc-mod, теперь он умеет вот так:

ghc-mod browse -d -o Data.Either

Left
Right
data Either a b
either :: (a -> c) -> (b -> c) -> Either a b -> c
lefts :: [Either a b] -> [a]
partitionEithers :: [Either a b] -> ([a], [b])
rights :: [Either a b] -> [b]

Добавил ещё несколько фич:

• Go to declaration (ctrl+shift+r по слову)
• Go to any declaration - команда выводит список всех деклараций во всех открытых файлах и cabal-проектах
• Теперь при старте ModuleInspector сканирует открытые директории и файлы, а не только после того, как активный файл сохранён
  

Пока, наверное, всё.

Исходники

Доделал, что хотел, вот список фич:

1. Поддержка cabal-dev
2. Поправлено куча ошибок с чтением настроек из других потоков *
3. Можно переключаться на ходу между cabal и cabal-dev, completion при этом обновляется
4. Completion теперь использует список импортируемых модулей файла для создания списка автодополнений. Т.е. добавили import Data.List, получили в списке ( Read more... )

Добавил примитивную поддержку cabal-dev, а также комманды clean/configure/build/rebuild/install для cabal и cabal-dev через Ctrl-Shift-P
Исправил ошибки, сборка теперь работает под Windows.

TODO:

1. Merge with HaskellBuddy
2. ghc-mod browse for imports: делать completion только для импортируемых модулей, в т.ч. стандартных
3. ghc-mod -s для cabal-dev
4. ghc-mod ( Read more... )

Подумалось мне про трансформеры монад, что если у нас есть натуральные преобразования из монад m и n в некую монаду l, то l - это их сумма, если добавить ещё и обратную функцию. Т.е. при наличии натурального преобразования m => t и n => t можем получить и m+n => t.

Попробовал я это представить прямо в таком виде:

data MonadSum m n a = MonadSum ( Read more... )

Продолжаю ковырять. Вроде как всё, что я хотел бы от поддержки туплов, Агда умеет (туплы мои). По сути получается удобная работа с гетерогенным списком. Я, правда, не писал ещё всякие map/zip и прочие, но, надеюсь, там проблем не будет.
http://hpaste.org/68922

Ковыряю Agda2
module if where open import proof open import bool open import list if_then_else_ : ∀ {l} {a : Set l} → (p : bool) → ((p ≡ true) → a) → a → a if true then t else f = t refl if false then t else f = f head₀ : ∀ {l} {a : Set l} → (ls : list a) → (not (empty ls) ≡ true) → a head₀ {_} {_} null () head₀ {_} {_} (cons x xs) p = x test₁ ( Read more... )

Наткнулся случайно на такие дела.
Это же замечательно:

record Monad {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  field
    F : Endofunctor C
    η : NaturalTransformation id F
    μ : NaturalTransformation (F ∘ F) F

open Functor F

field
    .assoc : μ ∘₁ (F ∘ˡ μ) ≡ μ ∘₁ (μ ∘ʳ F)
    .identityˡ : μ ∘₁ (F ∘ˡ η) ≡ idN
    .identityʳ : μ ∘₁ (η ∘ʳ F ( Read more... )

В прошлой записи мне дали ценные подсказки. Во-первых, проблема в том, что sequence не удовлетворяет требованиям и потому монадический трансформер из списка так просто не получить. Во-вторых, был задан более общий вопрос: переносится ли эндофунктор над Set в эндофунктор над Клейсли-категорией.
Посоставляв диаграммы (которых я тут не приведу), я ( Read more... )

Возьмём Клейсли-категорию для монады Writer. Затем определим функтор такой, что
F(a) = 1 + a * F(a) -- список
F(f) = id + f * F(f)
  -- null -> null
  -- (x, xs) -> (f x, F(f) xs)
где + и * в F(f) - choose и parcomp

Но в таком случае, если я ничего не путаю, не соблюдается F(f . g) = F(f) . F(g)

Действительно, возьмём f, пишущий "f" и возвращающий свой ( Read more... )