28 August 2009

Doing and being

I've been reading Sartre's Being and Nothingness again - it's very interesting!

I read it last year, but since then, all the ideas have become muddled in my mind - also I have a tendency to jump back and forth between the concepts I am struggling with, rather than read linearly and absorb at the author's intended pace, so I'm attempting to give it a much fuller read this time.

I just really want to share how cool I think this book is! Occasionally I get stuck and have to draw out his arguments in predicate logic. Thinking about it, it would be cool to encode his ontology into prolog maybe - then you could question details of his thought directly. Also to retrieve quotations.

Occasionally I find myself in bad faith - I work a lot sometimes to create cool things - and I feel that somehow that makes me cooler, but this is bad faith because I am seeking to escape what I am to be what I am not, and simultaneously to escape what I am not to be what I am.

So cheers to Sartre for letting me figure that one out :)

26 August 2009

pointless

This post is a literate haskell file.

I like the pointless style of programming - that is, functions do not mention the variables they act upon explicitly. While this is very common and cool, it's also a source of amusement - occasionally I find myself distract from a project by a need/desire/delusional whim to re-write various functions as pointless as possible. So here is a little one, it's nothing special.

> import Control.Arrow

> por1 :: (b -> Bool) -> (b -> Bool) -> b -> Bool
> por1 = curry $ curry $ uncurry (||) . (uncurry $ uncurry (&&&))

That is, por is a function which takes two predicates and input -
each predicate is from a polymorphic type b to a boolean
Apply both the predicates to the input, producing two boolean valies
Apply "Or" to these values to return one result.

There are automated tools to do this sort of obsfucation with haskell but I find my brain boils attempting to hack out this sort of "write-only" code. (this is a good thing)

Here is what the pointfree took makes of a pointful version* of the above:

> por2 = ((uncurry (||) .) .) . flip (&&&)

I like that, though the flip, in this case, is semantically irrelevant.

More about the pointless style
also comparison to unix pipelines
The question is: how to implement uncurry in bash? Next post, possibly. Hobgoblin has had the better of me tonight! :)

* the pointful version:

> por3 p q = uncurry (||) . (q &&& p)

22 August 2009

Delve tutorial

It occured to me that readers would be unable to decipher the last post without reading the tutorial, so I'll link that here:

Tutorial on the untyped delve core

21 August 2009

The Delve Type System

(EDIT: bogus logic fixed)

I've been working on the type system for Delve. Here lie the innovative features of the language.

It would be nice to infer the interface of objects, rather than an exact name. This is a much more Smalltalkish approach - an untyped language considers only the interface - the names are irrelevant. Consider this example: ( Warning, I haven't actually tested the examples - it's of little importance to the thought really )

In Haskell, consider the silly ADT

data Tree = Branch { tree :: Tree }

And the Haskell function, bound to the variable f:

let f = \ b -> tree b

Now say we have a Delve object corrosponding to the Tree adt.

(: Tree (Object.new))
(: Tree.tree
   (me ()
       (self)))

See here * for an example which constructs a class using the meta-object model.

And the corresponding Delve function, bound to the variable f:

(: f (fu (b) ((b.tree))))

Now with Haskell, the type checker will say: what is the type of 'tree'? It's 'Tree -> Tree'. Therefore f is of type 'Tree -> Tree'

Now what I'm trying to do with Delve is for Delve to say "b is a new mutant object of which I know nothing. However, it must have the method tree. Therefore, the type of f is 'Mutant with method tree, where tree is of type a -> a'

I think that's pretty cool.

To get this magic to work however, I have given Delve four type constructs. Firstly to explain the key concepts of unification and domination.

In Delve, a type is unified with another type if one type can be used in the place of another. This is a separate notion from equality - equality is a subset of unification.

Domination is where one type, (a type which is more concretely defined) actually replaces the other type in the type system. What seems to the type-checker as an initially polymorphic variable can be dominated into becoming a concrete variable in this manner.

So this is a first attempt at describing the various types.

An object: an object is a value of indisputable type.

For unification with another type, the two types must be objects, the objects must have the same name, and the types of both objects members must all be the same ( recursively considering these types ).

A mutant: a mutant is a value of disputable type.

A mutant can be unified with another mutant if the members of the first mutant are a subset of the second mutant of the same name - in that they set of the names of the first mutant is a subset of the second, all also that each of the intersection of the two sets of members unify.

A mutant also unifies with an object, if the above restrictions are met, but an object will dominate a mutant - that is, an object can be used as a function argument where a mutant is expected, but if an object is assigned to a mutant variable - the variable will become an object.

Mutants which unify can be merged, by safely putting the member types of both mutants into one new mutant. The changes must be propagated to any mutants which unified with the old type.

A function: Delve is strict and does not support curried function application, therefore a function can be simply represented by a list of types.

A function unifies with another function only if each of their types unify.

A polymorph: a polymorph will unify with any type, will be dominated by any other type.

The types arranged then in order of concreteness

Object, Function
Mutant
Polymorph

Now for an example, back back to our function:

(: f (fu (b) ((b.tree))))

The type checker will then type check this as follows – try to imagine you are the Delve type checker – this will be your thought process.

A function will be assigned to the variable f.

f will have the type of this function.

Since this function has one argument, the initial type which we will consider will be “Polymorph called a → Polymorph called b” (to use a Haskelly sort of notification”

So open a new scope, and let b be a new polymorph called a.

Now look at the code for this function.

A member of b, called tree, is being called.

So the type of b might be a “Mutant with with a member tree, where tree is a Polymorph called x”

This is ok, because this new type unifies with b's old type, since everything unifies with a polymorph.

Also, this type dominates b's old type. So b's new type is “Mutant with member tree, where tree is a Polymorph called x”

Tree is called of b, which is a polymoph called x.

So the return type of this function is a polymorph called x.

So the type of this function is 'Mutant with member tree, where tree is a polymorph called x → x'

So the type of f is 'Mutant with member tree, where tree is a polymorph called x → x'

Which is what we want. I think this is cool – but it has some problems. First, the rules for assignment and application will be formalized – this is useful – also it reveals the problems.

Assignment – assignment assigns a result to a variable. Assignment is correct if the type of the result unifies with the type of the variable. The type of the variable is always dominated by the type of the result. This means a polymorphic variable will be erased if say, an object is assigned to its place.

Application – actual arguments are applied to a function. The types of the functions formal arguments have already been decided and are not changed in a global sense.. The types of the actual arguments must unify with the types of the formal arguments. However, if the type of an actual argument dominates a polymorphic type in the formal arguments, all occurrences of the polymorphic type in the resultant type (local to this computation) are changed into the dominating type.

Say for our example, where f is 'Mutant with member tree, where tree is a polymorph called x → x'

If f is applied to a “Mutant with a member tree, where tree is of type Tree”, then locally, the type of f will become “Mutant with a member tree, where tree is of type Tree → Tree”. The result will then be of type “Tree”. However, when f is next used, its type will still be 'Mutant with member tree, where tree is a polymorph called x → x'.

Member lookup – looking up a member of a polymorph dominates the polymorph with a mutant type which possesses this member, and gives the member a new polymorphic type. Looking up a member of a mutant succeeds with the unification of the mutant with a new mutant as before. Looking up the member of an object succeeds if the object has this member. The resultant type, ie, the type of the member lookup, is the type of the member, once the appropriate unification (and perhaps domination ) has been applied.

Function creation – polymorphic arguments are introduced to represent each formal argument. Each formal argument is then dominated by the statements making up the body of the function. The return type is the type of the last statement in the function's body.

Method creation – same as function creation – exception the method imposes domination on the “self” - it can be only be assigned to an object, or within the local scope of that object, where the object unifies with this self.

*Delve has no class macro yet, so here is code which manipulates the meta-object model, allowing for the silly Tree class.

(: Tree (Object.new))
(: Tree.instance_methods (Object.new))
(: Tree.instance_methods.tree
   (me ()
       ((Tree.new))))
(: Tree.new
   (me ()
       ((: instance (Object.new))
        (: instance.class self))))

Either that or just use an object


Hmm, I must write a HTML pretty printer for delve...

20 August 2009

Writing

I am a semi-being. Not of thought, of drooling adrenaline. I exist for others, and they exist for me, and I see myself through them. But I would exist otherwise, without them but unable to see myself, like a book unwritten, a reality unfurled, a potential undiscovered. And these others, they are books unwritten too, for I cannot see them even now they can see me - but better unwritten, for finality is a tragedy, whether of books or for the dead. And I do hate a morbid party.

Today I saw a brown butterfly against a white wall but for a second it was a white butterfly against a brown wall. I wonder whether I should be taking sanity pills again!

Also I drank beer today, for the first time since the weekend. That was probably the longest I've gone without drink in months.

I started writing a story too. I used to get really flustered with trying to make every paragraph perfect, until I'd re-worked it so much that it was entirely unreadable. I've decided instead to hammer ahead, trying to write something which entertains, rather than worrying about little things like the quality of the prose :)

I'm always amazed by how much shit people talk. Really it's all in the perception. The other day, Lizzie and I were observing the new tap ( we have a new tap ). It is a tubalar breed, and I observed that while dispensing water it wobbles. It was fun watching it wobble. And not only this, it was about as concrete and solid an event as ever has been - it definitely wobbled, there was no question - and it wasn't a bizarre or surprising event. Predictable, deterministic, perfectly causal. Yet it was so funny and trippy and far out. How can such an event occur to two (mostly) sane individuals?

Anyway thinking about such things has prompted this small spate of writing which may continue wearily like the characters within. The other tragic thing, rather than just endings, is that in interesting books, people tend to die, shit, piss, puke ( well those three probably make enjoyable reading ), get raped, burned, stabbed, shot etc. It's such a shame! It's why I like cheesy horror films - mostly you want that sort of shit to happen to the annoying characters contained.

13 August 2009

Categorical joke

I thought up a joke about category theory,
though it's extremely bad!

There once was a poor endofunctor called Endo. Endo was so poor he
couldn't afford to undertake any more natural transformations, so he had
to borrow money from a loan shark.

But poor old Endo was sooo poor, he couldn't pay the money back! He got
more and more in debt to the loan shark until one day the loan shark
came over to his house to demand his dues.

So the loan-shark banged on the door and shouted "Hey you FUNCTOR! Give
me back my cash!".

"But I can't! I can't give you anything back!", cried the poor
endofunctor, from the upstairs window.

"And why not? You'd better give me the money" the loan shark asked.

"But I can't give you anything" moaned Endo, as he began to weep,
"Because I'm not co-pointed!"

(However, at this point in the joke, the loan shark was no longer needed
so he was garbage collected and Endo lived happily ever after.)

11 August 2009

Delve core

(Posted to the Haskell-Cafe mailing list)

Delve is a new programming language intended to bring the benefits of static type checking and functional programming to object-oriented design and development. It is an impure, eager language (Yes I can hear the groans of woe and cries for sanity already!)

Currently Delve supports:

Higher-order functions/first class functions
Anonymous functions
Lexical closures
First class continuations
Tail-call optimization
A meta-object model (classes are objects)
S-Expression based syntax.
Embedded Haskell expressions within Delve.

What it doesn't have:
Lots and lots!
Basically what I have is an de-sugared, untyped core language. An analogy could be made with Haskell core files.
I'm going to be working on the type system for next little while (I have a stack of paper and a pen right here!). Once that is implemented we'll see where to go.

Please see the TUTORIAL file included in the source for a brief outlook on Delve's syntax, semantics and planned type system.

However! If you're looking for a new project, and especially if you are an undergraduate, then I think Delve would be a good choice for these reasons:

It's written in a hybrid of Haskell and itself.
It's currently undergoing active development (by me and some pals). You're not going to be lonely!
It's quite powerful already, without too many lines of code (it's now just about 5.5KLOC - it's no goliath! )
It's a programming language: name a compiler which isn't a cool piece of tech! Ok, maybe you can but still, it's a chance to work on something non-trivial and interesting.
Quite honestly, I'm a bit of a fool - I am a math undergrad! So don't you feel foolish about getting involved if you're not a professorial chap! If you feel like it, get involved in the design, and push me the patches :)

It does require lots of love though! It was all hacked out rather quickly :)

Executables which Delve provides:

edc -- The Elgin Delve Compiler

The Elgin Delve Compiler currently supports two backends - the first to a bytecode format for execution on edvm, and the second is to a Haskell source code representation of Delve bytecode. This allows Haskell to be embedded within Delve, for the express purpose of extending and building edvm. edc is written in Haskell (GHC).


edvm -- The Elgin Delve Virtual Machine
The Elgin Delve Virtual Machine executes Delve bytecode files (.dcode format). Since part of the VM is actually driven by Delve bytecode, edvm can be considered a hybrid of Delve and Haskell (again GHC).

Delve continues the grand tradition of naming compilers after Scottish Cities (no, Elgin does not have a university).


Delve is released under the terms of the GNU GPLv3.

For more information on Delve, check my blog at http://killersmurf.blogspot.com/ and the Delve repository at http://github.com/elginer/Delve/

6 August 2009

Maintenance

Today I received two emails. The first one asked for a much needed feature in tagsoup-parsec - allowing user-supplied state, which I added.

However, the other email reported the fact that shpider no longer worked.

Shpider uses curl for a backend. The funny thing about curl is that it only writes cookies to a file when its cleanup function is called, rather than when it recieves them. However, in the original curl-bindings, this function was only called on garbage collection, through a foreign pointer finalizer. This resulted in some weird behaviour, like cookies being written at unexpected times. This is crippling if your program logs in to a website and then expects a cookie to be written to hold the session key.

So I forked the library to work on a solution. The obvious one is to call the finalizer manually, which worked before, but seems to crash now ( new GHC? ), so now I have to handle my own garbage collection, in order to get deterministic behaviour.

I really should put shpider in a git repository, to let others peer at it more effectively.

In other news, I hope in a couple of days I shall be able to publish the first component of a cool new piece of tech.... ooooh, the suspense.