luqui

data Set : Type where
    Comp : (Set -> Type) -> Set

elt : Set -> Set -> Type
elt (Comp f) = f

W : Set
W = Comp (\A => Not (A `elt` A))

Russell : Type

luqui

import Data.List (intercalate)

write :: String -> String
write = intercalate ". " . map (\word -> "Write " ++ show word) . words

howToWrite :: String
howToWrite = "How to write this book: " ++ write howToWrite

{-
>>> putStrLn $ take 1000 howToWrite

luqui

Really? <table> isn't available in markdown?

4

1	2
3

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

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

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

* 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