дыбр

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

October 2017

S M T W T F S
1 2 3 45 6 7
8 910 11 12 13 14
15 16 17 18192021
22232425262728
293031    

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Oct. 18th, 2017 08:30 pm
Powered by Dreamwidth Studios