дыбр

Oct. 24th, 2013 01:33 pm
juan_gandhi: (VP)
Вчера... вчера я где-то в полчетвёртого зафигачил новый парсер, запустил тесты на ночь на стейджинге, и в шестом часу ломанулся опять в город, на, блин, встречу категорщиков. До города-то доехал нормально, но в городе застрял на всяких там улицах. Да затрахало. Последний раз (в этом году). Заявился в офис Прези в 7:15, меня уже искали.

Ну офис ладно, мы проникли в конце концов; нас было шестеро в сумме. В комнате, куда мы пришли, на доске были остатки урока венгерского, и я обнаружил, что ха, на этом-то уровне mindent tudom. Должны были проходить третью главу книжечки Пирса - typed lambdas, categorical style. Ну и чо. Собралось опять половина новых; объясняй им, что за пределы такие... нет, что такое декартово произведение! И что за суммы такие! Короче, протрахались минут сорок с этой ерундой, потом как-то хитростью (без сопряженных функторов) протащили экспоненту.

Тут ещё новенький, Сергей, всё норовил возразить, в русском стиле, мол, нам эти ваши абстракции и даром не нать, у нас всё множества кругом, и можно ограничить дискурс малыми категориями - теория множеств, дескать, и есть основа вычислительных наук. На предложение охарактеризовать Cat было молчание. Я пытался добиться, какая польза вычислениям от аксиомы выбора. потом нарисовал пример неизмеримого подмножества отрезка [0,1]. Молчанье.

Ну ладно. Я уже совсем был почти pissed off. Плюс голодный; обещанной еды Прези не предоставило.

С божией и шахафовой помощью втянулись, наконец, в книжку. Дошли аж до примерно 20-й строки. Потом мне стали объяснять рулеса типовой лямбды; в частности, постоянно фигурировала какая-то гамма. У меня в книжке никакой гаммы не было, и я стал приставать, откуда взялась эта невидимая гамма.

И тут оказалось, что гамма невидима только у меня в книжке, а у остальных в книжке гамма есть. Пришлось мне руками вписывать гамму!

После чего Мэтью пошел к доске и стал расписывать смысл в общем-то простых рулесов. Но Мэтью тоже из Израиля, и гамму он писал как её писали финикийцы, в обратную сторону (гимель, ); ну чо.

Я же как этот стал приябываться к каждому рулесу. Ну типа вот вы говорите, что x имеет тип A × B - а это ж изоморфно B &time; A, так оно имеет и этот тип? Или чо? Или как?

Меня долго убеждали, что тип парсится в процессе валидации фразы, и определяется однозначно, но тут я совсем озверел - как вы нахер определите однозначно, если пределы в категории, как и вообще все сопряженные, определены с точностью до изоморфизма? Это же бред, почему unit имеет тип Unit, а не UnitUnit × UnitX?

И тут Шахаф сказал.

Дык. Для этого Воеводский HoTT и впендюрил, что типы не однозначно, а с точностью до изоморфизма определяются.

О блин. Мы вышли на гомотопическую дорожку. Уже Дан Пипони книжку читает, и ещё кто-то там в Гугле. Короче, надо всё бросать и переучиваться заново. Потому что у Пирса в третьей главе булшит. И что, никто не видел? Тьфу.

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

И вот едем мы, я какую-то музычку по радио поставил, и обсуждаем какую-то хрень ну типа как бы нам перекатиться с семинаром в Заливную, желательно в Маунтин Вью (и другого Мэтью ещё притащить - тоже израильтянин); и с Валерией да с Дэном согласовать, чтоб всем удобно было.

И тут Шахаф говорит - а, а кстати, в хаскеле все монады происходят от карриинга.

Чо?! О блин! Вот чо! Это же representable functors! Главное - пределы сохранять.

Перевариваю.

Ну и заодно, к слову, посмотрел как Максим жжет глаголом на киевском fprog:

http://www.youtube.com/watch?v=lJlqQDMpY3I&feature=youtu.be&a

Ну как мы уже поняли, всё не так просто. Но и не так уж запрещено.
juan_gandhi: (VP)
(эрланг превращается... эрланг превращается... ну и заодно свободные монады в одну строчку)

http://maxim.livejournal.com/418878.html
juan_gandhi: (Default)
Вот возьмём-ка монадку X2, из моего поста.

"Какая ж тут у нас монада? Монада берёт множество X и сопоставляет ему X×X. Монадная единица - диагональ (η(x) = (x,x)), а монадное умножение, X×X×X×X → X×X строится, согласно картинкам из начала этой части, из ε: (Y1×Y2, Y1×Y2) →(Y1,Y2) - проектированием по первой и последней координатам. μ(x1,x2,x3,x4) = (x1,x4)."

Так вот, а какие ж бывают алгебры над такой монадой? Нам надо, чтобы был f: A×A → A, соблюдающий условия:

f(a,a) == a

f(f(a1,a2),f(a3,a4)) == f(a1,a4)

Мне вот что-то сдаётся, что в условиях булевости и точечности (ну, скажем, в множествах) только проекция удовлетворяет такому условию. p1(a1,a2) = a1; p2(a1,a2) = a2.

Хотите попробовать порешать? По-моему, прикольная задачка. Хотелось бы найти, конечно, необходимые условия, при которых это так. Точечность на фиг не нужна, но булевость...
juan_gandhi: (Default)
Думаю, с чего начать, с комонады или с сопряженных... давайте-ка сначала пример с комонадой.

Итак, в предыдущей серии мы брали категории C=Set и D=Set×Set - множества и пары множеств, и два функтора, Δ(X) = (X,X) и Π((X,Y)) = X×Y.

Первый функтор - диагональ, он множеству сопоставляет пару, состоящую из двух экземпляров оного, а второй паре множеств сопоставляет декартово произведение; и эти функторы были сопряжены, Δ ⊣Π.

У функтора Δ на самом деле есть не только правый сопряженный, Δ ⊣Π, но и левый, Σ ⊣Δ. Что это за функтор такой? Давайте не надеятся на чудо, а просто его построим. Нам нужно, чтобы по (f1,f2): (Y1,Y2) &: ; (X,X) мы могли взаимно-ознозначно получать &alphal(f1,f2): Σ(Y1,Y2) → X.

Напомню, что стрелка (f1,f2) в Set×Set - это просто пара обычных стрелок (функций) в Set.

Заданы две функции, f1: Y1 → X и f1: Y1 → X. Что это нам даёт? Это нам даёт, взаимно-однозначно, функцию из непересекающегося объединения: Y1 ∐ Y2 → X.

Так что наш функтор Σ - это просто объединение двух компонент. Ну а так как он левый сопряженный к Δ, то композиция ΔΣ, которая для множества X возвращает X ∐X, является комонадой.

Думаю, понятно как определить ε: X.т∐X → X; а δ: X ∐ X → X ∐ X ∐ X ∐ X, как и во вчерашнем примере, складывает первую компоненту слева в первую компоненту справа, а последнюю - в последнюю.

Ну а теперь к монадам и сопряженным функторам.

Вот давайте вообще начнём с монады T: C → C, со всеми её монадическими законами (единица, умножение, ассоциативность умножения и единичность единицы).

Определим алгебру над монадой: это объект A и стрелка a: T(A) → A, обладающая правильными свойствами. А именно:
         


Я тут для простоты выбросил много скобок... ну что вы хотите, я же скальшик а не лиспщик.

Категория алгебр над монадой T в категории C обозначается CT.

Из алгебр, понятное дело, есть забывающий функтор UT. в категорию C - просто забудем, что есть какое-то действие. К этому забывающему функтору UT имеется левый сопряженный функтор FTC → CT, строящий по объекту X свободную алгебру, которая на самом деле выглядит так: μX: TTX → TX.

Откуда сопряженность, FT ⊣ FT? Если есть алгебра b: TB →B, и f: A → B, то имеет место коммутативная диаграмма


- которая всё и объясняет.

Итак, взяв любую сопряженную пару, можно построить монаду, а по монаде - сопряженную пару (свободный, забывающий). Очевидно, что монада, соответствующая этой паре, и есть исходная монада; но одной монаде могут соответствовать много разных сопряженных пар (их целая категория); пара (свободный, забывающий) - предельный случай. Вот другой предельны случай - категория Клейсли.

Возьмём монаду T: C → C и построим на её основе новую категорию, CT, состоящую из тех же объектов, что и исходная категория, но с добавлением стрелок. А именно, всякая стрелка f: :X → TY в C будет стрелкой f: :X → Y в CT. (Это, к примеру, если у нас монада Option, то теперь стрелками будут все частичные функции.) Композиция f;g определяется через ; все стрелки исходной категории превращаются в .

Так что имеется вложение ITC → CT; и к нему я хочу построить левый сопряженный, чтобы было KT ⊣ IT.

Эту сопряженность можно выразить как
f: ITX → Y  <====>  ?: X → KTY

но, по определению CT, это всё равно что задать
f: X → TY  <====>  ?: X → KTY


Определим KTY = TY - и на этом всё.

Для монады Option в множествах категорией Клейсли будет категория множеств и частичных функций, а категорией алгебр - категория множеств с выделенной точкой.

Для монады X2 в множествах категорией Клейсли будет категория множеств и пар функций, а категорией алгебр - категория множеств с заданной бинарной операцией.

Сказать мне вроде на эту тему больше нечего, если не подскажут, чего ещё добавить. Какие-нибудь специфические монады с комонадами?
juan_gandhi: (Default)
Итак, если у нас имеются две категории, C и D, и два функтора, F: C → D и G: D → C, мы говорим, что эти два функтора образуют сопряженную пару, F ⊣ G если имеется взаимно-однозначное соответствие
F(X) → Y  <====>  X → G(Y)


Для сопряженной пары мы вывели два естественных преобразования, η: IdC → F;G и ε: G;F → IdD.

Оказывается, если есть такие два естественных преобразования, для пары функторов, то они сопряжены.
Ну и правда, если есть f: F(X) → Y, то приложим к нему G, получим G(f): G(F(X)) → G(Y), и соединим это с ηX: X → G(F(X)), получим ту самую X → G(Y).

То же самое, по симметрии, проделывается и в другую сторону. Вообще, у меня тут половина рассуждений лишняя, потому что зеркальная симметрия ж (никаких бозонов).

Наши ηX и εY обладают чудесными свойствами:

   


Эти два чудесные свойства получаются в результате применения тех самых соответствий α и β, что были нарисованы в первой серии - попробуйте сами.

У нас есть теперь всё для монады и комонады.

Монада делается путём композиции, T = F;G; это функтор T: C → C. В качестве монадной единицы годится уже появлявшаяся у нас η, а в качестве монадного умножения (a.k.a. flatten) возьмём μX = G(εF(X)): G(F(G(F(X)))) → G(F(X)).

Единица оказывается единицей относительно монадного умножения, и умножение оказывается ассоциативно - всё это следует из описанных выше свойств сопряженных функторов.

Симметрично мы можем определить комонаду, путём композиции U = G;F.

Пример.

Возьмём категории C=Set и D=Set×Set - множества и пары множеств, и два функтора, Δ(X) = (X,X) и Π((X,Y)) = X×Y.

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

Эти два функтора сопряжены, Δ ⊣Π.

А именно, если есть (f1,f2): (X,X) → (Y1, Y2), то это задаёт отображение X →Y1×Y2, и наоборот, отображение в декартово произведение Y1×Y2 задаёт пару отображений, по компонентам.

Какая ж тут у нас монада? Монада берёт множество X и сопоставляет ему X×X. Монадная единица - диагональ (η(x) = (x,x)), а монадное умножение, X×X×X×X → X×X строится, согласно картинкам из начала этой части, из ε: (Y1×Y2, Y1×Y2) →(Y1,Y2) - проектированием по первой и последней координатам. μ(x1,x2,x3,x4) = (x1,x4).

Кто любит симплициальные категории, увидит тут различные краюшки и рёбрушки, но это ладно, это мы лучше не будем трогать.

"Практический смысл" в программировании у этой монады вот какой: есть двоичный флаг; и наши данные от него зависят - в одном случае вызов возвращает Y1, а в другом Y2. Ну и если у нас есть функция, зависящая от того же флага, то нам надо как-то комбинировать и сплющивать; это же Reader Monad, сведённая к двоичному флагу. Ну вот эта монада и есть.

Вопросы?

(Завтра продолжу, хочу показать, как из монады можно построить сопряженную пару, и не одну.)
juan_gandhi: (Default)
1, 2, 3, 4, 5, 6, 7, 8, 9, 10

Весь нижеупомянутый код расположен на гитхабе у котят.

Пример. Моноид и Накопление Ошибок


Read more... )
juan_gandhi: (Default)
В разных там WriterMonad требуется, чтобы внутре был моноид, и возникает иной раз такое ощущение, что и везде нужен моноид. Ан нет, бывает и полугруппы достаточно.

Скажем, Option[T], где Т - полугруппа, можно считать моноидом - к полугруппе присоединяется внешний нуль.

def sum(maybeX; Option[T])(maybeY: Option[T]) = maybeX match {
  case Some(x) => maybeY match {
    case Some(y) => Some(x+y)
    case None    => Some(x) }
  case None => maybeY
}

Так получается, что тот нуль, что был в T раньше, теперь не будет нулём.

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

Это, заодно, ответ на мой старый вопрос - шо за моноид в мапредьюсе. Да вот этот, с присоединённым нулём.
juan_gandhi: (Default)
http://vpatryshev.blogspot.com/2012/06/cake-pattern-practices.html

Только что запостил. Там всё примитивно (надеюсь); если чего не хватает или неправильно, буду рад выслушать.
juan_gandhi: (Default)
trait Applicative[T[_]] extends Functor[T] {
  def pure[A](a:A):T[A]
  def ap[A,B](tf:T[A=>B]): T[A] => T[B]
  def map[A,B](f:A=>B) = ap(pure(f))
}

abstract class Applicable[A, B, T[_]](fs: T[A=>B]) {
  def <*>(at: T[A]):T[B]
}
abstract class Lifted[A, B, T[_]](f: A=>B) {
  def <@>(ta:T[A]): T[B] // in Haskell it is <$>; can't use $ in Scala, and can't have lt;&s> either.
}

trait RichApplicative[T[_]] extends Applicative[T] {
  implicit def applicable[A,B](tf:T[A=>B]): Applicable[A, B, T]
  implicit def lift[A,B](f: A=>B) = new Lifted[A, B, T](f) { def <@>(at: T[A]) = ap(pure(f))(at)}
}

trait Traversable[T[_]] extends RichApplicative[T] {
  def traverse[A, B](f: A => T[B])(as: List[A]): T[List[B]] = as match {
    case Nil => pure(Nil)
    case head::tail => lift(cons[B] _) <@> f(head) <*> traverse(f)(tail)
  }

  def dist[A] = traverse(identity[T[A]] _) _
}


Work in progress. I'm on page 5. (dumb, eh)

Comments? Ideas?
juan_gandhi: (Default)
Yesterday at Intel we Martin Odersky was giving an informal talk on how things are etc. Mostly on the features of 2.10. Pretty cool. Macros are experimental, if included. Anyway; good stuff.

There were over 50 people in total, and a kind of warm atmosphere; after the talk we stood chatting for about an hour, this and that, and functional, and monads (everybody gives me a nudge as soon as the word "monad" is mentioned... talking about myself - Martin seems to remember my name, weird.)

Next two meetings are next week; Monday at Twitter ("Scala at Twitter" - they are pretty advanced indeed), and Wednesday at LinkedIn ("Scala at LinkedIn") - this one I'm planning to attend.

It's all on meetup, so there.

P.S. [livejournal.com profile] xeno_by, I talked with Bill Venners regarding macros; seems like he's looking for more details, to use this stuff in his scalatest; do you have a fresh preso? I'd forward it to him. Or you could.
juan_gandhi: (Default)
def take[X](n: Int) = { var i = 0; (x:X) => {i = i + 1; i <= n}}   
take: [X](n: Int)(X) => Boolean

scala> 2 to 100 by 7 filter (take(5))                                  
res5: scala.collection.immutable.IndexedSeq[Int] = Vector(2, 9, 16, 23, 30)
juan_gandhi: (Default)
Still struggling implementing McBride/Paterson in Scala.
def K[env,a](x:a) = (gamma:env) => x
implicit def ski[env,a,b](ef:env=>a=>b) = new { 
  val S = (ea:env=>a) => (gamma:env) => ef(gamma)(ea(gamma))
}

val add = (i: Int) => (j: Int) => i+j
  type Env = String => Int
  def fetch(x: String) = (env: Env) => env(x)

  trait Expr
  case class Var(x: String)        extends Expr
  case class Val(i: Int)           extends Expr
  case class Add(p: Expr, q: Expr) extends Expr
  def Ke[T](x:T) = K[Env, T](x)
  
  def eval(exp: Expr): (Env => Int) = exp match {
    case Var(x) => fetch(x)
    case Val(i) => Ke(i)
    case Add(p,q) => (Ke(add) S (eval(p))) S (eval(q))
  }

eval(Add(Var("one"),Add(Var("three"), Val(11))))(Map("one" -> 1, "two" -> 2, "three" -> 3))



Kind of funny how one has to bypass the lack of Hindley-Milner... oh, whatever.

Will explain all this later, when I'm done with McBride-Paterson.
juan_gandhi: (Default)
А скажите люди добрые, бывает такая теория типов, чтобы ещё была какая-нибудь группа симметрии (да хоть 2, инволюция), и чтобы все функции эту симметрию поддерживали?

Не знаю, понимаете ли вы, к чему я клоню, но если можно как-то нарисовать такие типы, с симметрией, то дальше я вам покажу Hask, где не всяка монада аппликативна, ха-ха-ха-ха-ха!
juan_gandhi: (Default)
src
interface Lam<X, Y> {
  Y apply(X x);
}
 
// http://en.wikipedia.org/wiki/SKI_combinator_calculus
class SKI {
  public static <A, B, C> Lam<Lam<A, Lam<B, C>>, Lam<Lam<A, B>, Lam<A, C>>> s() {
    return new Lam<Lam<A, Lam<B, C>>, Lam<Lam<A, B>, Lam<A, C>>>() {
      public Lam<Lam<A, B>, Lam<A, C>> apply(final Lam<A, Lam<B, C>> f) {
        return new Lam<Lam<A, B>, Lam<A, C>>() {
          public Lam<A, C> apply(final Lam<A, B> g) {
            return new Lam<A, C>() {
              public C apply(final A a) {
                return f.apply(a).apply(g.apply(a));
              }
            };
          }
        };
      }
    };
  }
 
  public static <A, B> Lam<A, Lam<B, A>> k() {
    return new Lam<A, Lam<B, A>>() {
      public Lam<B, A> apply(final A a) {
        return new Lam<B, A>() {
          public A apply(final B b) {
            return a;
          }
        };
      }
    };
  }
 
  public static <A> Lam<A, A> i() {
    return SKI.<A, Lam<A, A>, A>s().apply(SKI.<A, Lam<A, A>>k()).apply(SKI.<A, A>k());
  }
}
juan_gandhi: (Default)
Now you can include links to diagrams with the option of editing.




⛤◯▯△
juan_gandhi: (Default)
[livejournal.com profile] sassa_nf высказал недоумение, если не больше, по вопросу как это мы вставляем ap между нашими аппликативными штучками, как это? Я думал, э, всё просто.

Протрахался с 7 до 11. Вот код с примером; а текст потом поправлю, спать же уже пора, ё.

  import scala.collection.immutable._

  trait Functor[T[_]]{
    def map[A,B](f:A=>B)(ta:T[A]):T[B]
  }

  trait Applicative[T[_]] extends Functor[T]{
    def pure[A](a:A):T[A]
    def ap[A,B](tf:T[A=>B])(ta:T[A]):T[B]
  }

  implicit def applicablize[A, B](fs: Set[A=>B]) = new {
    def <*>(as: Set[A]) = (for (f <- fs; a <- as) yield f(a)).toSet
  }

  implicit object AppSet extends Applicative[Set] {
    def pure[A](a: A) = Set(a)
    def ap[A,B](fs:Set[A=>B])(as:Set[A]):Set[B] = (for (f <- fs; a <- as) yield f(a)).toSet
    def map[A,B](f:A=>B)(as:Set[A]) = ap(pure(f))(as)
  }

  val p = AppSet.pure((s:String) => "'" + s + "'")
  val p2 = AppSet.pure((first: String) => (second:String) => first + " " + second)
  val names = Set("Jedi", "Michael Valentine")
  p <*> names
  val lasts = Set("Smith", "Frazer")
  p2 <*> names <*> lasts
juan_gandhi: (Default)
Subclassing errors, OPP, and practically checkable rules to prevent them

P.S. I believe the problem is that with stateful objects, we do not know exactly which category are we dealing with; roughly speaking, for class A subclassing class B, there are actually two monads, with a natural transformation from one to another; and we think we have a functor from, not sure yet, one Kleisli category to another, or from one Eilenberg-Moore category to another, or even an interesting relationship between two categories of adjoints generated by the monads.

Have to look closer; maybe this explains the problem with "Liskov substitution".

Profile

juan_gandhi: (Default)
juan_gandhi

June 2017

S M T W T F S
     1 2 3
4 5 67 8 9 10
11 12 13 14 15 16 17
18 19 20 21 22 23 24
252627282930 

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jun. 25th, 2017 08:50 pm
Powered by Dreamwidth Studios