juan_gandhi: (VP)
Came to a conclusion that it may be easier to use the idea of "evidences"; e.g. a truth table is an evidence; a proof is an evidence; but then we basically have a topos below (an evidence of a conjunction is a tuple, and an evidence of an implication is a function).

So, it's a type theory.
juan_gandhi: (VP)
Find the type error in the following Haskell expression:

if null xs then tail xs else xs
juan_gandhi: (VP)
"There is nothing that can possibly be done in this case. The laws of parametricity say that the signature:

def foo[T]: T

can never be satisfied for all T unless you do something dodgy like throw an exception, or not return at all – ie. something that actually is of type Nothing."
juan_gandhi: (VP)
Consider me an idiot, but I do not see anything in type theories that could not be much simpler expressed categorically. Okay, if we have types. If we don't, then it's λ, no? With variations. Also, reading all these κ and ζ theories I get a weird feeling that they are solving problems that were solved 60-70 years ago.

And they constantly use the word "set"! Something like "we introduce a natural numbers object, bla-bla-bla, and we have a set of arrows from such an object to a type..." omfg. That's ridiculous.

Anyway. Sorry.
juan_gandhi: (VP)
In DFW, the airport.
While on the plane, managed to build the correct empty type (and false);

Thank you [livejournal.com profile] migmit; it was not exactly the way you said, but pretty close.

So there.

Will give a talk about it next week.


Aug. 31st, 2014 03:40 pm
juan_gandhi: (VP)
If your constructor has a boolean parameter, you actually have two different types.
juan_gandhi: (VP)
Everybody knows that a binary tree is defined by a formula T(x)=1+x*T2(x), where x is the type of the value that the tree contains.

For the beginners: A tree is either empty (=1) or a triple: (x, t1, t2) where t1 and t2 are also binary trees of the aforementioned kind.

So there. Easy. You can see that this is a quadratic equation, and that it can be represented as a cubic root on a complex plane... it's not about this; let's see how we can store changes in trees, that is, differences, that is, derivatives.

dT/dx = T2 + 2*x*T*dT/dx, whereby we have
dT/dx = T2/(1-2*x*T)

Oh, wait, you probably heard already that List(x) is defined by a formula List(x)=1+x*List(x), right? Either empty (=1) or a pair (ok, a product) (x, List(x)), right?

but this equation, List(x)=1+x*List(x) has a solution, List(x)=1/(1-x). Remember this.

Now 1/(1-2*x*T) is a list, List(2*x*T)

So dT/dx = T2 * List(2*x*T)

An update of a tree can be represented as two trees and a list of triples (bool, x, T), where T is a tree.
But what is it?

The two trees are left and right subtrees of the point-of-change; and the list of triples is the path from the root to the point of change; each element of the path being this:
- left or right
- the changed value
- the intact subtree

On this picture you see gray left, black right, and the path is red values with brown intact subtrees.

Cool eh?

Note, I did not use any particular programming language.

Source: http://www.youtube.com/watch?v=YScIPA8RbVE&noredirect=1


Feb. 26th, 2013 11:06 pm
juan_gandhi: (VP)
Народная теория категорий, через типы.

Категория состоит из типов и функций; каждая функция - из какого-то типа А в какой-то тип Б; имеется композиция функций, имеется тождественная функция. Имеется особый тип, Unit, aka (). Функция из () в тип А называется инстансом типа А.

И понеслась. Функтор F - это отображение, заданное на типах (т.е. для каждого типа X задан какой-то тип F[X]), у которого имеется ещё F.map[A,B]: (A => B) => (F[A] => F[B]).

Мономорфизмы, эпиморфизмы.
Подкатегории, декартовы произведения, пулбаки, пределы, копределы, и т.п., монады.
Категория Клейсли, категория алгебр.
Катаморфизмы и проч.

Декартова замкнутость.

Классификатор подтипов (a.instanceOf[X])

Предпучки, топологии Гротендика, топосная логика, семантика Крипке-Жуаяля.
Модальная логика.


juan_gandhi: (VP)
Spent a couple of weeks trying to figure out what exactly is it. Looked it up in Wikipedia, in Scala, in Haskell, in popular articles. Now I think I know what it is; here's my vision. Please pardon my English and my cheap, simplified Math.

1. Type Class is an Algebraic Theory

An algebraic theory is a rather abstract notion. It consists of variables of one or more types, a collection of operations, and a collections of axioms.

1.1. Example
Monoid. Just one variable type; two operations: a binary operation and a nullary operation (that produces a neutral element), and axioms: associativity and neutral element neutrality. Integer numbers can be perceived as a monoid, say, using multiplication as the binary operation and 1 as the neutral element.

1.2. Example
Vector space over a field. We have two types of variables, vectors and scalars. Scalars can add, subtract, multiply, divide, have a zero, a one; vectors can add, subtract, have a zero, can be multiplied by a scalar. We can also throw in scalar product of two vectors.

2. But Can We Express A Theory As Trait (interface, in Java)?

On many occasions, yes. You can define a pure abstract trait (or, in Java, just an interface) that defines the operations, e.g. for a monoid:

trait Monoid {
  def neutral: Monoid
  def binOp(another: Monoid): Monoid

Notice, we do not specify any axioms. In languages like Scala, Haskell, Java, we cannot. It takes Agda to handle axioms.

We have a problem here that the if we try to introduce a specific kind of monoid, the result of binOp does not belong to that kind; so we have to be more careful and design our trait keeping in mind we are going to extend it, like this:

trait Monoid[Actual] {
  def neutral: Actual
  def binOp(another: Actual): Actual

Now we can define something like
class StringConcatMonoid(val s: String) extends Monoid[StringConcatMonoid] {
  def neutral = new StringConcatMonoid("")
  def binOp(another: StringConcatMonoid) = new StringConcatMonoid(s + another.s)

It works... but well, the new class is not exactly a String class, right? That's the problem, we cannot throw in the new functionality into String.

Suppose for a moment we could (we can do it in JavaScript ad libitum). What would we do with Ints then? What binary operation, addition? multiplication? min? max? There might be more.

Now let's disambiguate.

2 3. Model

When we defined a trait without implementation, we described a theory. When we started building specific implementations, we define a model for our theory. There may many models for the same theory; the same structure may be a model of a variety of theories. We have to be able to express this relationship.

In the example above we made StringConcatMonoid a model of Monoid theory. We were lucky, we had just one type; imagine we had more than one. Then there's no way to inherit anything. And we are still not happy that we cannot define binOp on Strings themselves; we look at Haskell, and seems like they do it easily.

In Haskell, models are called instances (of a type class); in C++0x (please excuse my misspelling) they are called models (and theories are called concepts).

In Haskell one can define
  class Monoid m where
    binOp   :: m -> m -> m
    neutral :: m

and model it with lists (strings are lists in Haskell):
instance Monoid [a] where
    binOp = (++)
    neutral = []

We can do it in Scala, kind of more verbosely.

object A {
  implicit object addMonoid extends Monoid [Int] {
    def binOp (x :Int,y :Int) = x+y
    def neutral = 0
object B {
  implicit object multMonoid extends Monoid [Int] {
    def binOp (x :Int,y :Int) = x ∗ y
    def neutral = 1
val test :(Int,Int,Int) = {
    import A._
    println(binOp(2, 3))
    import B._
    println(binOp(2, 3))

In one case we used one binOp, in another we used another. We can define fold that implicitly accepts an instance of Monoid, and provides the required operation, but that's beyond the topic of this talk.

3. Important Remark
We could probably start thinking, hmm, how about just parameterized types, what's the difference? Say, take List[T], is not it a type class? We have abstract operations, independent of the type T, and so it is also not a specific type, but a class of types, right?

Not exactly. It is a totally different thing, unfortunately written in the same style. Here we have a functor: given a type T, we produce another type, List[T], uniquely determined by the type T, and whose operations (almost) do not depend on what is T.
While we could make it into a type class, if the polymorphism here were ad-hoc, we normally do not.

4. That's Not It Yet

Next I'll show how we can restrict the scope of certain operations to certain subtypes, of the type that we pass as a parameter.

please correct me where I'm wrong
juan_gandhi: (VP)
Сидит Андрей Петрович Ощепков на крутом бережку Енисея и читает книжку "Гильбертовы Пространства в Задачах и Решениях"; подходит мужик, глядит на обложку, и спрашивает Андрея Петровича: "а шо це за параша, Гильбертовы Пространства?" 

Итак, мой предыдущий пост я практически объявляю полной фигнёй.

Кроме одной фразы - type class - это класс типов. Остальное фигня.

Как я понимаю, класс типов можно определить а) параметрически: List[T] - это класс списков с элементами типа T; в хаскеле для этого есть лихой термин type family b) через уравнение:
class Eq a ...; в скале это можно задать приблизительно.

Сегодня Дэвид Анджеевски на скальном митапе вообще задвинул термин type class pattern, и на мой вопрос, не знает ли он формального определения тайпкласса сказал, что нет, не знает.

Вот ещё линки.
typeclassopedia, by John Kodumal, Atlassian - слов и примеров много, определения нет.
что сказал Дебасиш - это типа скорее паттерн тоже
Stackoverflow: какая польза от тайпклассов? ("а сёдла на них есть?")
Moors, Pissens, Oderski, "Generics of Higher Kind" - тут скорее намёки на тему тайпклассов, наряду с техничным рассуждением на тему шо в скале уже таки есть
"oop vs typeclasses" - по мне так скорее философия, с намёками, что, э, может быть таки тайпклассы - это параметризованные типы, не?

gentle haskell - здесь объясняют, что как раз не, объявляем через уравнения, а определяем или параметрически, или адхок.

Ну вы поняли, да? Я не понял. Только вижу, что тайпклассы - это что-то вроде многообразий, и не пора ли уже просто откровенно пойти пошукать шо за гомотопическая теория типов такая, и не отвечает ли она на вопросы.

Надеюсь на продуктивную дискуссию.
juan_gandhi: (Default)
А скажите люди добрые, бывает такая теория типов, чтобы ещё была какая-нибудь группа симметрии (да хоть 2, инволюция), и чтобы все функции эту симметрию поддерживали?

Не знаю, понимаете ли вы, к чему я клоню, но если можно как-то нарисовать такие типы, с симметрией, то дальше я вам покажу Hask, где не всяка монада аппликативна, ха-ха-ха-ха-ха!
juan_gandhi: (Default)
(from Miles Sabin's post)
// Encoding for "A is not a subtype of B"
trait <:!<[A, B]

// Uses ambiguity to rule out the cases we're trying to exclude
implicit def nsub[A, B] : A <:!< B = null
implicit def nsubAmbig1[A, B >: A] : A <:!< B = null
implicit def nsubAmbig2[A, B >: A] : A <:!< B = null

// Type alias for context bound
type |¬|[T] = {
 type λ[U] = U <:!< T

def foo[T, R : |¬|[Unit]#λ](t : T)(f : T => R) = f(t)

foo(23)(_ + 1)   // OK
foo(23)(println) // Doesn't compile

juan_gandhi: (Default)
Spent two hours studying this.

Somehow we felt extremely happy after finishing this.


juan_gandhi: (Default)

October 2017

1 2 3 45 6 7
8 910 11 12 13 14
15 16 17 18192021


RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

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