luqui

More developments in the design of Sequent:

The modeling power of Sequent may be stunted by its limited ability to talk about objects. I keep invoking Skolem functions and the like in my models, which then need to leak into other propositions and I am then flooded by unnecessary equality assumptions just to say something that should be simple. This paragraph could be completely wrong, as I have no evidence for this, this is just the picture of the frustration in my mind.

But speaking of pictures, I had a new one of Sequent today. Instead of a Coq-like environment where you have hypotheses and a goal, I pictured an object environment (I have written about that phrase before); you always have a valid program, and you are merely manipulating it. (A valid program may need witnesses that you do not have, so in that sense you can't use it until more work is done).

When you look at objects in this environment, you always have a set of assumptions (it would not be Sequent without that!), and you have a se

luqui

(\g \h -> 
 (\x -> [[apply 'g 'x] = 'h]) = (\x -> ['g = [lambda 'x 'h]]))

-- x is dynamically bound above; usages of this property will have x free in h. 
-- Not sufficient, I think.

-- Here's a (rather verbose) way to define (er, assume) W = \x. x x

\W (x -> ['W apply 'x] = ['x apply x'])

luqui

I keep trying to think about this Sequent thing but keep getting distracted by you-know-who. Unless you are not me, in which case you may now be wondering who. It's that bodhisattva from last summer, the one who sorta drove me crazy and made me have an emotional breakdown and spend the next nine months healing. So, how about that? Perhaps I am stronger now.

Anywho, I'm just playing piano on Pearl street a lot. Making my rent and food, hopefully some left over to take with me to New Orleans, if I am in fact going there, or to buy a Haken Continuum, or something. When I'm not doing that I'm hanging out with Amanda (not to be confused with she-who-shall-not-be-named above) or practicing Liszt's Mephisto Waltz no. 1, which I ought to have to Pearl-performable in a couple weeks.

And now I am sitting here listening to pandora, and journaling. It was going to be about Sequent but that has not gone according to plan at least in the first two and a half paragraphs. Maybe it was like an introduction, just to ge

luqui

I admit, I am stuck. I don't know what to do next on this project. I have a very simple javascript repl, it really is nothing fancy, and the first innovative feature I have I can't figure out how to implement.

The feature is abstraction. My working example, not anything practical, has been

two = 1 + 1              --> 2
four = two + two         --> 4
eight = four + four      --> 8

This represents an interactive session in which the programmer was experimenting with things, tweaking them, trying to get things to come out just right for two. Now that the correct answer has come out, the programmer wants to abstract his solution to work for any value of two. I picture a little button next to two (maybe in a menu -- whatever), which will purge two from the definitions and move it to the environment of the functions that use it; roughly

luqui

Since I am doing this music thing, it may be a while until I do any leisurely programming again and who knows how my interests will have shifted by then. So I would like to take this time to dump my current vision of Sequent, the encapsulation-free programming environment. First I will give some of my inspirations for the idea. I will then move on to the basic concepts and operation of the environment.

Inspirations

The first inspiration is from Haskell in highly polymorphic code, or if you like, from Coq. For hard programming problems I often write down what I have and what I need. Let's take an example, writing the Monad instance for Cont.

newtype Cont r a = Cont { runCont :: (a -> r) -> r }

instance Monad (Cont r) where

luqui

All this lisp programming has fired up my language design interested again -- mostly seeing how bad common lisp is, and how great it could be in my idealized details-not-figured-out-and-possibly-don't-exist world.

What I'm working with right now is seeing a language implementation entirely as a structural catamorphism -- or perhaps more alluringly, a semantic map. This is an extensible, Lisp-style language, and we see language extensions as extending the semantic domain. What I hope will result is a language that has very nice denotational reasoning properties, despite being very customizable and extensible (the latter being what usually destroys the former).

The semantic domain is often made up of mathematical objects which are complex to specify, and in the spirit of Lisp we would like this to be a small language base upon which more can be built. So I believe it is too much to ask of the language to specify semantic domains in full detail. However, perhaps we may keep the domains themselves abstr

luqui

{-# LANGUAGE RankNTypes  #-}

import Prelude hiding (zipWith)

newtype ChList a = ChList { fold :: forall b. (a -> b -> b) -> b -> b }

nil :: ChList a
nil = ChList $ \f z -> z

cons :: a -> ChList a -> ChList a

luqui

{-# LANGUAGE RankNTypes, TypeOperators #-}

data Monoid m = Monoid { mempty :: m, mappend :: m -> m -> m }
data Generator a m = Generator { monoid :: Monoid m, singleton :: a -> m }

newtype Free s = Free { getFree :: forall a. s a -> a }

mkMonoid :: (forall s. f s -> Monoid s) -> Monoid (Free f)
mkMonoid f = Monoid {
    mempty = Free (mempty . f),

luqui

{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies #-}

-- related to http://hackage.haskell.org/trac/ghc/ticket/1496

type family F a
type instance F Int = Int
type instance F X   = Int -> Int

class Fable a where
    fify :: a -> F a

luqui

Goals

It's hard for me to make progress on opusmodus when I don't feel like I can sufficiently modularize my changes. The file is 700 lines, and that does not include test support. It is too much to manage at once. Now I have an algorithm for splitting & beaming which involves a number of auxiliary concepts (a theory of intervals and linear transformations), which don't seem at home at the top level. I want to be able to package them up in a pretty way, and this is an opportunity to explore some of the abstract flexiblility I have been pondering for the last two and a half years.

In my case, there is a concept of intervals, which comes with some operations and laws. There is also vocabulary associated with intervals, which may involve some other concepts. This is all independent of their implementations -- the operations and the vocabulary. Traditionally, the vocabulary is a collection of functions implemented in terms of the basic operations on intervals; however, the key I have been explori