rocketnia

#lang racket

; vector-representation-selection.rkt
;
; A vector type `my-vector` that automatically switches to a byte
; string representation if it's only reachable via values the contract
; `(my-vectorof byte?)` has been imposed on. Test this at the REPL
; like so:
;
;   (require (submod "vector-representation-selection.rkt" demo))

rocketnia

Overhauled Cene syntax:


In an s-expression context, end of file accumulates zero s-expressions, then ends.


In an s-expression context, whitespace does nothing, then proceeds as usual.


In an s-expression context, a span of identifier text accumulates one s-expression consisting of the corresponding string, then proceeds as usual.

rocketnia

-- A response to the challenge at https://twitter.com/arntzenius/status/876405069012504577

type Test = String -> Bool
type Re = Test -> Test

match :: Re -> Test
match a = a null

rocketnia

When someone shares or installs a Cene library, it consists of several parts, which together (in uncompressed form) determine its hash:

- A UUID indicating what spec of the Cene language is intended.
- A source file tree.
- A string containing a single Cene expression to evaluate to get a function that takes a reference to the source file tree, monadically performs macroexpansion side effects in its own sandbox (where every name is based on the library's overall hash), and results in a sink value. The side effects may include looking up other libraries by hash, which allows multiple libraries to import common names and constructors for communicating with each other.

The Cene language UUID accounts for built-in definitions, parser syntaxes, file tree archive formats, and macroexpansion side effect models that may vary between Cene versions. A UUID is preferable to a signature, a public key, or a a DNS host for this purpose; Cene implementations will inevitably implement divergent support for the same UUIDs, 

rocketnia

Some of the usual calculus of constructions rules:

Gm |- type A
---
Gm, x : A |- x : A

Gm, x : X |- F : Y
---
Gm |- (\x : X -> F) : (Pi (x : X). Y)

rocketnia

The 30 NES games I might've picked for the NES Classic Edition, if it were up to me:

Boulder Dash
The Karate Kid
Kirby's Adventure
Krusty's Fun House
Little Nemo: The Dream Master
Lode Runner
Mega Man
Mega Man 2

rocketnia

An entity can be a pair of entities, with the first being in command of the second's content and execution. For instance, the first can be an imperative computation that only invokes the second computation when (and if!) it finishes. As another example, the first entity can be an interpreter, manually walking over the second entity and updating it. The first entity has exclusive control over the second, except inasmuch as some other entity has control over it. The second cannot even refer to the first except by doing open-ended communication side effects.

All working memory in the system is partitioned into an infinite binary tree, where at each level, the first branch is in command of the second's content and execution. For instance, the first branch can be an imperative computation that only invokes the second computation when (and if!) it finishes. As another example, the first branch can be an interpreter, manually walking over the second branch and simulating it. The first entity has exclusive control o

rocketnia

TODO: Fill in the average lengths marked by ???.

{
	"origin": ??? [
		119+,
		???,
		???
	],
	
	"tweetHomage": 119+ [

rocketnia

Two of the achievements in Nameko Rhythm are awarded when you've seen
at least 50 and at least 100 King Nameko. To optimize my grinding for
these, I recorded the song lengths:

00:01:44.618 okurahomamikisaa
00:01:43.981 kurobuchika
00:01:50.064 chairo no kobin
00:02:12.087 za entaateinaa
00:02:07.895 yorokobi no uta
00:02:11.999 nameko no uta

rocketnia

; The problem with this isn't the paradox but the fact that the
; paradox is possible to create fully inside a single Tenerezza
; operation.

(swap-continuation original
  ; We could do the same thing as we do on the other side, but we do
  ; something simpler. We just send the back-and-forth continuation
  ; back to itself. This also demonstrates that we don't need
  ; `original` to be in scope here to produce the paradox (though it
  ; would be trivial to surround this whole thing with two more