ghc-mod 1.11.5
eye
voidex

Немного пропатчил 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]


SublimeHaskell: Go To Declaration
eye
voidex
Добавил ещё несколько фич:
  • Go to declaration (ctrl+shift+r по слову)
  • Go to any declaration — команда выводит список всех деклараций во всех открытых файлах и cabal-проектах
  • Теперь при старте ModuleInspector сканирует открытые директории и файлы, а не только после того, как активный файл сохранён

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

Исходники



SublimeHaskell
eye
voidex
Доделал, что хотел, вот список фич:
  1. Поддержка cabal-dev
  2. Поправлено куча ошибок с чтением настроек из других потоков *
  3. Можно переключаться на ходу между cabal и cabal-dev, completion при этом обновляется
  4. Completion теперь использует список импортируемых модулей файла для создания списка автодополнений. Т.е. добавили import Data.List, получили в списке всякие zipWith4.
  5. Теперь в completion есть не только свои модули в том же cabal-project'е, но и все установленные в cabal'е или в текущем cabal-dev'е
  6. Добавлен ghc-mod check и ghc-mod lint. Есть также check+lint, показывающий вывод обоих сразу. При этом lint показывается как hint'ы (без различий на error/warning) **
  7. Добавлен stylish-haskell, как весь файл, так и селектированные участки **
Автор сейчас занят, поэтому pull request пока висит, взять можно здесь.

* Львиная доля ошибок, благодаря которым под виндой SublimeHaskell не работал вообще была связана с тем, что запрещённое согласно документации чтение настроек из другого потока стабильно падало под Windows, а под Ubuntu вроде как падало, но редко, что не мешало работать. Плюс почему-то все сплитят строки при помощи split('\n'). Вообще говоря, ни одного серьёзного коммита у меня не обошлось без того, чтоб под виндой это как-то не отозвалось.
** Спасибо dotcypress за предложение смержить с его HaskellBuddy




TODO:
  • goto declaration
  • search for declarations по всему проекту (как Ctrl+R)

SublimeHaskell
eye
voidex
Добавил примитивную поддержку 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 check + ghc-mod lint при сохранении
  5. Fix ModuleInspector for Windows

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

Попробовал я это представить прямо в таком виде:
data MonadSum m n a = MonadSum {
  monadSum :: forall t. (Monad t) => (forall b. m b -> t b) -> (forall c. n c -> t c) -> t a }


И вот, что получилось:
maybeIO :: Maybe a -> StateT s IO a
maybeIO Nothing = error "Nothing"
maybeIO (Just v) = return v

eitherIO :: Either String a -> StateT s IO a
eitherIO (Left e) = error e
eitherIO (Right v) = return v

stateIO :: State s a -> StateT s IO a
stateIO act = StateT $ return . runState act

bla :: MonadSum Maybe (MonadSum (Either String) (State Int)) String
bla = do
  n <- liftR $ liftR get
  case n of
    0 -> liftL Nothing
    1 -> liftR $ liftL $ Left "Error"
    2 -> liftR $ liftL $ Right "Ok!"
    _ -> do
      liftR $ liftR $ put (n `div` 2)
      s <- bla
      return $ show n ++ s

testBla :: Int -> IO String
testBla = evalStateT $ unlift maybeIO (unlift eitherIO stateIO) bla

Запуск:
*MonadSum> testBla 0
*** Exception: Nothing
*MonadSum> testBla 1
*** Exception: Error
*MonadSum> testBla 2
"Ok!"
*MonadSum> testBla 3
*** Exception: Error
*MonadSum> testBla 4
"4Ok!"
*MonadSum> testBla 8
"84Ok!"
*MonadSum> testBla 7
*** Exception: Error


Полный код тут.

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

Agda2
eye
voidex
Ковыряю 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₁ : ∀ {l} {a : Set l} → list a → a → a
test₁ ls v = if (not (empty ls)) then head₀ ls else v

test₂ : ∀ {l} {a : Set l} → a → a
test₂ v = head₀ (singleton v) refl
Tags: ,

Agda2
eye
voidex
Наткнулся случайно на такие дела.
Это же замечательно:
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) ≡ idN
Tags: ,

Klesli + List 2
eye
voidex
В прошлой записи мне дали ценные подсказки. Во-первых, проблема в том, что sequence не удовлетворяет требованиям и потому монадический трансформер из списка так просто не получить. Во-вторых, был задан более общий вопрос: переносится ли эндофунктор над Set в эндофунктор над Клейсли-категорией.
Посоставляв диаграммы (которых я тут не приведу), я пришёл к выводу, что да, если коммутирует левая-верхняя диаграмма оттуда же (остальные мне не пригодились), что для списка наверняка не верно (хотя я не проверил).
Т.е. если можно получить монаду над ST, используя натуральное преобразование TS -> ST, то можно и эндофунктор T перенести на категорию Клейсли (с монадой S). Однако данные требования избыточны, так как мы не комбинируем монады, а переносим эндофунктор.
Есть для этого какое-то название и не налажал ли я, не знаю.


Kleisli + List
eye
voidex
Возьмём Клейсли-категорию для монады 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" и возвращающий свой аргумент, и g — пишущий "g".
Тогда f . g допишет "fg".
F(f) [1,1,1] — "fff"
F(g) [1,1,1] — "ggg"
F(f . g) [1,1,1] — "fgfgfg"
F(f) . F(g) [1,1,1] — "fffggg"


Кто виноват и что делать?

?

Log in