0x20

Хаскель предлагает достаточно удобный для большинства задач уровень абстракции - алгебраические типы, сравнение с образцом, классы типов. Забираясь выше, легко попасть в ловушку не решения проблемы предметной области, не достижения цели, а решения проблемы отображения решения проблемы предметной области на фиксированный уровень абстракции и ни ангстремом ниже.

Здесь (thesz)

Видели уже наверное:
http://absurdopedia.wikia.com/wiki/Haskell

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

Заинтересовал меня всё таки kurilka тотальным ФП, а у deni_ok и thesz я понахватался ссылок и умных слов. Ну, ещё и dependent types в стороне не остались.

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

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

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

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

Если у кого то есть материалы по теме, накидайте сюда плз - потом как руки дойдут обязательно прочту всё-всё-всё :-)

Брат прислал: классная игрушка. 288 резинок - если не убьют, то закидают.

Вот видео оттуда:

Небольшое вступление.

Есть такой модуль Control.Applicative, в котором определён класс Applicative

class Functor a => Applicative a where
    pure :: a -> f a
    <*> :: f (a -> b) -> f a -> f b

т.е. он чуть шире Functor (за счёт pure), и чуть уже Monad. Золотая середина - полезно, когда нам от монад нужен только return.

( тут мне непонятно )

Давно ничего не писал, обновлю журнал.

Вот парень классно прикололся.



Пробежал позавчера HL2E2. Атака страйдеров отражается так - убиваешь охотников машиной, при этом у тебя скорее всего будут тяжёлые потери, но охотник валится сразу; либо гравипушкой закидываешь их какашками - так ты более мобилен и сил для игр и роста остаётся гораздо гораздее. Дальше просто - бомбу-липучку к пузу и биг-бада-бум!! Ах да! Ещё я бомб вокруг себя побросал, чтобы их не ждать в телепорте.

Просто балдею. Уже несколько раз поглядел.

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

Для equational reasoning в Haskell можно (иногда нужно) пользоваться GHC Rules (На Haskellwiki), чтобы написанное было читабельным и maintainable, а скомпилированное эффективным. А для нахождения нужных правил можно воспользоваться Theorem for Free. Например, его автоматической выводилкой. Или использовать free / ft команды lambdabot-а.

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

Это я всё мечтаю. Нарисовал нужные типы данных, сформировал по ним типы функций для работы над ними, автоматически построил их реализацию, автоматически построил правила, выбрал нужные для оптимизации. А дальше работаешь легко и непринуждённо. Это идеал, разумеется. Но я уверен, что частично эту работу можно автоматизировать. Типа того, что при доказательстве Coq'ом ему надо указывать стратегии, так же и здесь при реализации тела функции надо направлять "думатель".

Это вообще возможно? А то у меня каша в голове.

Официальный сайт токипоны.

Уроки токипоны:

^[RUS]Токипона на wikibooks (переведённые от jan Pije). Классика. Учитесь по этим урокам.
^[RUS]Уроки от jan Lekalo. Это даже не уроки. Парень учит токипону и по ходу обучения рассказывает про неё. По моему первый обучающий ресурс на русском.
^[RUS]Уроки на лингвисто от jan Eliki. Неоконченные, но проникнутые духом токипоны. Есть красивая азбука от Lament.

Общества, группы и т.д.

WIKI на TP.
TP на LJ.
^[RUS]TP на русском LJ.
TP группа на yahoo.

Персональные странички

jan Pije. Тексты, картинки, музыка. Есть сценарий "В поисках священного Грааля" Монти Пайтона.
jan Jakopo. Частота употребления звуков. Панграммы.
jan Ke. Гимны, молитвы.
Потом допишу, неохота вспомнить.

Письменность

Тенгвар
Скоропись или что то вроде этого. Не помню.
Хангыл. Самое симпатичное по мне. Сэмпл.
Иероглифы. Прикольно.
Иероглифы неоконченное

Послушать, посмотреть

shinan с 9:22 до 13:41 прикольно так болтает.
Песенки от Pije
Ещё где то лежало "mama pi mi mute o". Что то не найду сходу.

А у #tokipona дня три такой топик:

jan Lome li jan pi toki pona. ona li jo e jan lili sin. ona li mije. pona!

приятно чёрт возьми :)

Это ж надо умудриться родиться в самую короткую ночь в году!
Теперь у меня два рака. Когда подрастут, буду пить пиво с раками.

На RSDN технические работы.

( Read more... )

P.S. А ещё я сегодня видел в метро парня, читавшего распечатку "Знакомство с языком Haskell" или что то в этом духе ;-)

P.P.S. А ещё я подумал, что изобрёл слово "индексикация" как перевод indexitis (болезнь использования (!!) в Haskell), а оно оказывается существует реально и означает совсем-совсем другое :-(

Удивительно быстро прошёл Episode One



Жду - не дождусь Episode Two



А ещё я всё это могу играть, потому что у меня сгорел компьютер, и я взял новый.

Читал статью Bernie Pope "Getting a Fix from the Right Fold" из The Monad. Reader Issue 6. В ней решается задачка о написании dropWhile через foldr. В частности, эта задачка решалась в Graham Hutton "A Tutorial on the Universality and Expressiveness of Fold" через таплы.

У меня удивительно быстро получилось решить эту задачку. Решение было эквивалентным решению 2 в статье.

( Подглядеть )