luqui

import Control.Monad.Random
import Control.Monad.Writer

type Sim = Rand StdGen

-- returns the series of rolls, with the final 6 omitted (implied)
simGame :: Sim [Int]
simGame = do
    roll <- getRandomR (1,6)
    if roll == 6

luqui

Here is a section of a message I sent to Francois-Regis Sinot regarding his paper 
Complete Laziness: A Natural Semantics
http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/sinot-wrs07.pdf
---------------

I have simplified the problem down to this expression:

(\z. (\x. \y. x) (\w. z)) I I I

Where I is the identity function.  Preprocessing, this translates to (with some manual simplifications):

luqui

import Data.Ratio
import Data.List (partition)

-- Riemann's rearrangement theorem.  @rearrange target rs@ takes a sequence @rs@ whose sum converges but
-- does not converge absolutely, and rearranges its terms so that its sum converges to @target@.

rearrange :: (Ord a, Fractional a) => a -> [Rational] -> [Rational]
rearrange target rs = uncurry go (partition (> 0) rs) 0
    where
    go pos neg accum | fromRational accum < target = let (p:ps) = pos in p : go ps neg (accum+p)

luqui

Joao F. Ferreira asks the question:

Given a finite binary string, repeatedly change a pattern 00 to 01 or 11 to 10.  Will you ever stop?

Theorem: yes, always.

Proof: By strong induction on the length of n: any series of valid substitutions on any string of length n eventually terminates.

Notice that both substitutions keep the first character fixed.  For example, if the string starts with 01, then no substitution
will ever make it start with anything but 01.  

luqui

@spencertipping says "Similarly, the Twin Prime conjecture will never be proven independent; 
it will only remain an unsolved problem. Independent -> true."

Let me try to paint a picture of the Twin Prime Conjecture (TPC) having been proven independent 
of, let's say, ZFC.  That means "ZFC + TPC" is consistent, and so is "ZFC + ~TPC".  Since both 
of these are consistent, neither of them is concretely falsifiable.  Let's see how:

ZFC+TPC: there are infinitely many twin primes.  "Pick any number, you will find a twin prime 
above it."

luqui

* Show documentation about an object as you are typing/selecting it, no matter what the context.

* Allow verifiable but informal documentation: NonZero(x), where NonZero doesn't have a computable definition, but it is to be verified by the programmer as an "assertion".  Maybe it bubbles up (seems like it should, since it's a statement without proof).  What if it can't because the relevant variable escapes?

* Remember to commit to "write first, refactor later".  E.g. copy,paste,modify should share whatever code was not modified.

* Max hates reading code -- he much prefers to debug.  Seeing concrete values, allow concrete model to interpret abstract code.

* Collaborative editing.

luqui

I have a bunch of sketches like this lying around in my home directory, and I'm sure that when I change computers again I will probably forget them. So I'm switching to github for my sketches.

This is a generalization of types, using propositions instead. Not intended as a high-assurance formal verification system, just as a guide like types. But more expressive than representation types.

In informal haskelly-mathematical language I might write something like this:

Definition: i is an index for xs if i is a natural number < length xs.

Definition: If i is an index for xs, then xs !! i is defined by:

(x:xs) !! 0 = x

luqui

I find myself wanting an image-based functional environment, like a persistent ghci. I want to use it to track my TODO list, do quick one-off computations, store miscellaneous data and analyze it. Basically it's an environment where I can store my stuff that has the power of a Turing complete functional language. Like spencertipping's self-modifying perl scripts, but functional instead.

I'd also like to design it well. It's kind of a hacky purpose, but I might as well put some thought into its design and apply some of my recent ideas about modularity. In such an environment everything is constantly changing, and yet it ought to be purely functional, because pure functions are cool. So the module system has to be able to handle such a dynamic environment -- reusing old code in new contexts.

In an interactive environment, we are not usually designing for modularity. Instead we just enter expressions, save values away, inspect them, and enter more expressions. I would like to reuse any value I have give

luqui

Ok so I keep having the same idea over and over again. Maybe that means I like it.

This time I'm phrasing it like this: combining spencertipping's perl objects with functional ideals and distributed references a la Udon. These objects can have computational content (like perl objects, unlike Udon) and are defined in terms of an explicit abstract basis (unlike both).

Having tried to write this several times, I really want to be minimal about it. Not minimal as in perfect and beautiful -- minimal as in a small amount of work. I can give it water and sunlight later.

But first, as with all my recent projects, I have to determine what I mean by an abstract basis. I'm beginning to believe the idea is not reliant upon, but connected to the idea of types. A basis without types is just made of names, which are sufficiently ambiguous that they cannot be methodically searched or computationally combined (nor is their usage clear without examining their definition). Types allow the computer to see what is going

luqui

Our task is to characterize a relationship between an abstract syntax tree and concrete syntax, much like the development in [Invertible Syntax Descriptions by Tillmann and Ostermann][1]. We have an additional constraint, however. We aim to make the mapping interactively editable -- that is, convert editing commands on the text to transformations on the abstract syntax.

For example, consider a simple arithmetic grammar with precedence. Given this abstract syntax tree (in S-expression notation):

(plus 3 4)

which is pretty-printed this way:

3 + 4