lomeo: (лямбда)
Две библиотеки, о которых узнал из френд-ленты. Понравились.

1. mmtl via [livejournal.com profile] permea_kra.

Очередная библиотека монад-трансформеров с фишкой. Позволяет не определять для каждой монады инстанс каждого монад-класса. Таким образом модуль с ReaderT не будет ничего знать о MonadWriter, тем не менее инстансы для

(а) MonadWriter w => MonadWriter w (ReaderT r (Writer w))
и
(б) MonadWriter w m => MonadWriter w (ReaderT r (WriterT w m))

будут выводиться. Т.е. теперь мы пишем свой монад-трансформер и у нас автоматом есть инстансы для всех имеющихся монад классов.

К сожалению, (а) и (б) реализованы как отдельные инстансы. Была бы ещё возможность описать это в отдельном - типа
MonadWriter w i, MonadTrans t => MonadWriter w (t i)


Написано, что "Inspired by the paper /Functional Programming with Overloading and Higher-Order Polymorphism/, Mark P Jones"

2. Coroutine via [livejournal.com profile] nponeccop.

lightweight session types для описания протоколов. Индексированная монада для представления линейных типов, собирание типов с помощью комбинаторов типов. Понравилась реализация дуальности типа клиента и сервера - очень просто и красиво.

Подробнее в презентации Haskell Session Types with (Almost) No Class
от Jesse Tov. Есть видео, но я его не смотрел.
lomeo: (лямбда)
[livejournal.com profile] nealar сейчас в haskell@c.j.r показал на partial signatures от Олега.

Смысл в том, чтобы иметь возможность задавать отдельный констрейнт на тип функции, а всё остальное пусть выведется автоматически.

Второй случай рулит.
lomeo: (лямбда)
К чему я так подробно расписывал получение свёртки для розы? Очевидно, что интуитивно получить её можно сразу. Так я обычно и делаю, воспользовавшись методом размерностей, пардон, программированием "от типов". Возможно, так делаете и вы. Я хочу показать главный недостаток этого подхода - он неформален.

Read more... )

В данном конкретном случае нам очень сильно помогает Curry-Howard, но он не гарантирует уникальности доказательства (реализации), т.е. этот метод не формализуем. А вот на основе ТК, думаю, можно построить CataEval.
lomeo: (лямбда)
Когда я только разбирался с бананами, линзами и т.д. задача описания катаморфизма для розы:
data Rose a = Rose a [Rose a]

вызывала у меня большое затруднение.

Read more... )
lomeo: (лямбда)
Расширения типа fundep или MPTC обычно понятны бывают сразу, ну, по крайней мере, их идея. А вот чтобы разобраться с ошибками при инстанциировании класса, придётся разобраться.

Read more... )
lomeo: (лямбда)
Только недавно понял, что это то же самое, что и GADT:

data Z
data S n

data family List n a
data instance List Z a = Nil
data instance List (S n) a = Cons a (List n a)

--например
cadr :: List (S (S n)) a -> a
cadr (Cons _ (Cons x _)) = x


Только их ещё и расширять можно. Так что алгебраические типы данных, которые можно выписывать в разных модулях уже есть :-)
lomeo: (лямбда)
Заинтересовал меня всё таки [livejournal.com profile] kurilka тотальным ФП, а у [livejournal.com profile] deni_ok и [livejournal.com profile] thesz я понахватался ссылок и умных слов. Ну, ещё и dependent types в стороне не остались.

Подумал, что total fp будет неплохо смотреться для программирования на типах - гарантия завершения будет тут очень кстати.

К сожалению, "по семейным обстоятельствам" я сейчас не в силах заняться чем нибудь серьёзно, поэтому всё, что я здесь пишу - скорее для себя, чтобы не забыть. Написано очень нудно (это тоже для себя, извините - я тупой) и сумбурно (а это так получилось).

Итак что здесь? (чтобы вы решили читать или нет)
Здесь размышления о том, как должен работать тайпчекер в системе с зависимыми типами. Я пытаюсь придумать приёмы, позволяющие строить гарантировано завершающиеся доказательства/опровержения.

Итак, о чём думал, пока ужинал макаронами. )

Если у кого то есть материалы по теме, накидайте сюда плз - потом как руки дойдут обязательно прочту всё-всё-всё :-)
lomeo: (лямбда)
Допустим у нас есть тип (X a), где X ::= T x y z ... Тут важно, что "a" последнее.
Тогда если "a" хотя бы в одном конструкторе данных стоит слева от стрелки, то этот тип нельзя сделать функтором (instance Functor) так, чтобы соблюдались законы над функторами, нес па?

deriving

Jan. 12th, 2007 05:51 pm
lomeo: (лямбда)
Неожиданно обнаружил, что при включенном -fglasgow-exts для newtype можно делать deriving любых классов, экземпляром которого уже является обернутый тип.

newtype Stream a = S [a]
    deriving (Functor, Monad, Show)

А я дурак сижу пишу инстансы.

UPD: Читайте ещё извращений про deriving. На моём 6.4.2 не работают.
UPD 2: А вот и описание этой фичи.
lomeo: (лямбда)
Оказывается, есть и такая вещь в Хаскеле. Существует как расширение системы типов, есть ограничения, пользы большой не вижу, но пусть будет.

При dynamic scoping за связывание переменной отвечает вызывающий код, а не вызываемый.

Пример

function foo()
{
    print x; // x имеет динамическую область видимости.
}

function bar()
{
    var x = 5;
    foo(); // вот здесь x и привяжется.
}


то же самое на Haskell )
lomeo: (лямбда)
Рассматривая тип data S a = S a (S a) я увидел, что его нельзя сделать монадой - не будет работать либо первый, либо второй закон монад. Кто знает, есть ли какие то правила, позволяющие вычислить (или хотя бы почувствовать), что такой то тип не может быть монадой?
lomeo: (лямбда)
Кстати, есть такой интересный способ мышления, когда для написания функции я думаю о её типе и вывожу реализацию из типа. Я его достаточно часто использую в Haskell. Это вообще распространённая практика? Объясню на знакомом примере: например, мне надо написать функцию bind для State монады:

пример )

Многие так делают? Может быть есть еще ситуации где типы сильно помогают?
lomeo: (лямбда)


  1. Имеем функцию f x y z = ....

  2. С помощью лямбдабота переводим в pointfree стиль.

  3. Меняем:

    • (.) на B

    • ($) на I

    • flip на C

    • ap на S

    • join на W

    • const на K





Ничего не забыл?

UPD: О! Задачка!
На что надо поменять liftM, liftM2 и т.д.?
lomeo: (лямбда)
Сегодня прочитал о associated data types - вещь, согласно SPJ менее `tricky`, чем fundeps . Действительно, очень красиво. Жаль, что пока нет реализаций этой красивой идеи (сырой phrac пока не считаем).
вкратце )
lomeo: (лямбда)
Прочёл этот великолепный труд, который мне советовал [livejournal.com profile] polter.
По крайней мере понял откуда растут ноги у fold/unfold для произвольного типа. Я это и раньше чувствовал, но теперь получил формализованный вариант :-)

немного колючей проволоки на Хаскеле )

Кстати, там во второй главе ошибка. В самом конце при описании параморфизма (скобки, разумеется, колючие):

tails = (Cons(Nil, Nil), ⊕), где a⊕(as,tls) = Cons(Cons(a,as),tls)

это неверно, потому что даёт только первый tail (сам список), а не сохраняет последующие. Надо:

a⊕(as,tls) = Cons(Cons(a,as),Cons(as,tls))

Profile

lomeo: (Default)
Dmitry Antonyuk

December 2015

S M T W T F S
  12345
6789101112
131415 16171819
20212223242526
2728293031  

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 24th, 2017 03:51 pm
Powered by Dreamwidth Studios