1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
|
# 026 — 앱 계약: 1.0에서 얼릴 것
작성일: 2026-10-13. 상태: 설계. 지금 있는 앱 계약을 수식으로 적고, 1.0에서 얼릴 것과 1.0 전에 다시 세울 것을 가른다. 구현은
바꾸지 않는다. 번호에 대해: 139가 "026이 될 것"이라 부른 루프마다의 프로그램은 만들지 않았다(139의 뒷말). 이 번호는 앱 계약에 쓴다.
사용자의 말(2026-10-13):
- "세상의 그 어떤 명세와 개념이든 pure 생태계(vega, aup포함)에서 구현을 가장 유연하고 견고하게 해내야해. 추상화와 input ->
output으로 가는 과정은 얇고 직관적이고 빠르게."
- 1.0 전에는 호환을 챙기지 않는다. 얼마든지 갈아엎고 깎으며, 의미론적·수학적으로 불변할 최대의 아웃풋을 목표로 한다. 호환은
1.0부터다.
- 표준이란 기존 것을 이어받는 것이 아니라 Pure 생태계 안의 검증이다. 최고의 효율을 위해 바깥이 Pure에 맞춘다. JSON과 HTTP/1.1은
그대로 받는다(하이브리드).
- 기존의 추상화 층이 정말 필요한지를 계속 의심한다.
## 쉬운 말로
- Pure에는 두 부분이 있다.
- **앱 계약**: 이벤트는 트랜잭션이고, 상태는 저장되고, 보기는 상태의 함수이며, 메시지는 한 번 적용된다.
- **계산의 언어**: 핸들러와 보기 안의 값과 연산이다.
- **앱 계약은 이미 불변에 가깝다.** 플랫폼이 바뀌어도 이 문장들은 바뀌지 않는다. 이 문서는 그것을 수식으로 적고, 1.0에서 얼릴
후보로 둔다.
- **계산의 언어는 패턴의 모음이다.** 명령 90개와 상태 종류 7개가 판마다 앱의 패턴 하나씩을 일급으로 넣으며 자랐다. 그래서 세상의
명세 대부분을 아직 담지 못한다. 그것은 [140](../research/140-spec-suite.md)이 재고, 다음 설계가 다시 세운다.
- **계약 안에도 의심할 것이 있다.** 입력과 보기의 종류, 커서와 인덱스, 키별 문서, 수의 모델, 예산의 단위, 고정 한도다. 아래
"의심" 절에 둔다.
- **근거.** 지금의 구현과 그 검사다([008](008-module-format.md), [011](011-pure-transport.md), [015](015-boundary-meaning.md),
[017](017-apps-on-one-host.md), [018](018-lifetimes-and-computation.md)). 새로 잰 것은 없다.
- **다음 결정.** 140의 결과로 계산의 핵을 설계한다.
## 계약
### 앱
앱 A = (Σ, I, H, V, O):
- Σ는 상태의 선언이다. 상태마다 이름, 타입, 초기값, 수명(저장되는 것과 transient)이 있다. 상태의 값 s ∈ S는 저장되는 값과
transient 값의 짝이다.
- I는 입력이고, 입력마다 이름과 페이로드의 모양이 있다.
- H는 입력마다의 핸들러들이고, 소스 순서대로 돈다.
- V는 보기다. 인자를 받을 수 있다.
- O는 출력, 곧 보내는 메시지의 모양이다.
### 이벤트는 전함수다
이벤트 e = (입력, 페이로드, t)다. t는 호스트가 주는 시각이다. **시간은 입력이다.**
step_A : S × E → (S × Out*) ⊎ Fault
- **실패의 종류.** Fault는 다음과 `require`의 거절이다: `divide`, `non_finite`, `clamp`, `limit`, `not_found`, `encoding`,
`exists`, `memory`, `overflow`, `work`.
- **원자성.** step이 Fault를 내면 상태는 그대로이고 출력도 없다.
- **끝남.** step은 언제나 끝난다. 실행량 예산 W(명령 수, 기본 2^28)를 넘으면 `work`로, 메모리 몫 M(저장 형식의 바이트, 기본
2^28)을 넘으면 `memory`로 끝난다. 그래서 step은 전함수다.
- **결정성.** step은 함수다. 같은 모듈과 같은 이벤트열이면 어느 기기에서나 같은 상태, 같은 출력, 같은 실패를 낸다. 실패는 같은
자리에서, 같은 종류로 난다. 한도를 명령과 바이트로 세기 때문이다(017). Pi, WSL2, M3 Mac에서 `pure-run` 1,053번이 같은 출력을
냈다([114](../research/114-across-machines.md)).
- **역사는 접기다.** s_n = step(s_{n−1}, e_n). 앱은 결정적인 상태 기계(밀리 기계)다.
- **이벤트의 값**(`let`, 이벤트의 리스트, 메시지의 행)은 step 안에서만 산다.
### 보기는 커밋된 상태의 순수 함수다
view_v : S_c × Args → Value ⊎ Fault
- S_c는 마지막 저장의 스냅숏이다. 보기는 시각을 읽지 않고, 보내지 않고, 상태를 바꾸지 않는다. 이벤트와 같은 예산 안에서 끝난다.
- 표 보기의 칸은 물을 때 계산된다. 10만 항목에서 20행을 그리면 20행만 계산한다. 뜻은 함수이고, 게으르게 계산하는 것은 구현이다.
### 내구성: 보이는 역사는 커밋의 앞부분이다
- 저장 한 번은 마지막 저장 이후의 이벤트들을 한 커밋으로 공개한다. 전부 보이거나 하나도 보이지 않는다.
- 성공을 알린 이벤트는 저장됐고, 실패를 알린 이벤트는 흔적이 없다. 응답은 저장 뒤에 나간다. 묶어 저장할 때도 그렇다.
- 저장이 실패하면 마지막 저장 이후의 이벤트가 모두 되돌려진다. 그래서 밖에서 보이는 역사는 언제나 커밋된 이벤트열의 앞부분이다.
- 저장 결과를 모르면(`uncertain`) 앱은 다시 시작할 때까지 저장하지 않는다. 거짓 성공을 내지 않는다.
### 전달: 순서대로, 한 번
- 보냄은 이벤트의 일부다. 실패한 이벤트는 보내지 않은 것이다. 저장을 되돌리면 그 사이의 보냄과 번호도 돌아간다.
- 출력마다 1부터 번호를 붙인다.
- 받는 앱은 보낸 쪽마다 들은 번호를 상태와 같은 커밋에 두고, 그 이하의 번호는 다시 적용하지 않는다. 그래서 효과는 순서대로 정확히
한 번이다.
- 앱이 거절한 메시지도 전달된 것이다. 그 효과가 거절이다.
- 노드 사이에는 연결이 없다(011). 링크의 전송 상태(키 에폭, 번호, 확인, 허가)는 저장소의 행이고, 앱 상태와 같은 커밋에 든다.
### 경계: 받아들인 값은 어느 길로 나와도 같다
[015](015-boundary-meaning.md):
- 수는 비트까지(0의 부호만 빼고), text는 바이트까지, bool은 `true`나 `false`로, i64는 자릿수 하나까지 같다.
- 받아들일 수 없는 값은 들어오는 모든 길이 거절하고, 거절한 사건은 아무것도 남기지 않는다.
### 교체: 이름이 상태를 잇는다
- 모듈을 바꾸면 이름과 종류가 같은 상태가 남는다.
- 레코드가 바뀌면 이름과 타입이 같은 필드를 옮기고, 새 필드는 기본값으로 채운다. 이전 스크립트는 없다.
- 수식으로는 이름으로 정한 사상 μ : S_old → S_new 하나다.
### 한 호스트의 여러 앱
[017](017-apps-on-one-host.md):
- 앱은 실행 영역이다. 상태의 소유자가 하나라서, 한 앱은 한 번에 한 스레드에서만 돈다.
- 한도는 결정적인 단위(명령, 바이트, 요청 수)로 센다. 실패는 그 앱에서 멈춘다.
- 앱을 가르는 것은 검증기와 예산이다. 호스트 자신의 결함은 모든 앱의 운명이다. 이것을 프로세스 격리라고 부르지 않는다.
## 이 계약이 없애는 층
| 보통의 층 | 계약에서 | 근거 |
|---|---|---|
| DB 서버, 스키마, 이전 스크립트 | 선언한 상태가 곧 영속 상태이고, 교체는 이름으로 잇는다 | 008, [092](../research/092-tpcc.md) |
| 트랜잭션 코드와 되돌리기 처리 | 이벤트가 트랜잭션이다 | 008 |
| ORM과 직렬화 층 | 저장 형식이 곧 상태의 값이고, 선 위의 바이트가 곧 저장한 기록이다 | 011, 015 |
| 아웃박스, 메시지 큐, 멱등 키, 재시도 | 보냄은 이벤트의 일부이고, 받는 쪽은 들은 번호를 저장한다 | 008, [078](../research/078-app-connections.md) |
| 연결 관리(핸드셰이크, 재연결, 풀) | 연결이 없고, 전송 상태는 저장소의 행이다 | 011 |
| 캐시, 캐시 무효화, 읽기 복제 | 보기는 커밋된 스냅숏에서 돈다 | [080](../research/080-snapshot-reads.md) |
| 클라이언트 상태 관리, 가상 스크롤 | 보기는 상태의 함수이고, 칸은 물을 때 계산한다 | 008 |
| CLI·GUI·웹·API를 따로 짜기 | 같은 보기와 입력이 표면마다 쓰인다 | [010](010-surfaces.md), Vega |
## 의심: 계약 안의 용의자
기존의 층을 의심하듯 Pure 자신의 층도 의심한다. 아래는 지금의 계약에 들어와 있지만, 구현이나 한 앱의 패턴이 뜻이 된 것으로
보이는 것들이다.
1. **입력의 종류.**
- 지금: 키(누름과 뗌), text, 타이머, 메시지가 따로 있고, 초당 60번 오는 `frame` 이벤트도 있다.
- 의심: 기기의 패턴이 계약에 들어왔다.
- 후보: 입력은 모두 이름 있는 필드를 가진 메시지 하나이고, 키, 글자, 틱은 표면이나 호스트가 만드는 메시지다.
2. **보기의 종류.**
- 지금: 수, text, 표, bool, i64.
- 의심: 표는 값이 아니라 물을 때 행을 계산하는 함수다.
- 후보: 보기는 일반 값(중첩 포함)을 내고, 게으르게 계산하는 것은 구현의 성질로 둔다.
3. **커서와 인덱스.**
- 지금: 둘 다 상태의 종류다.
- 의심: 둘 다 "편집을 따라가는 위치"다. 넣기와 지우기를 따라 움직인다.
- 후보: 열(text, 리스트) 안의 앵커 하나.
4. **키별 문서.**
- 지금: v2의 `DOC`, `REPLACE`, 기준 리비전.
- 의심: 키 있는 리스트와 겹친다.
- 후보: 없앤다.
5. **수의 모델.**
- 지금: binary64가 기본이고 정수는 2^53 아래에서만 정확하며, i64와 u32(경계)가 따로 있다.
- 의심: f64 더하기에는 결합법칙이 없어서, 접는 순서가 답을 바꾼다.
- 정할 것: 정수와 실수의 관계, 그리고 접기의 순서 규칙.
6. **예산의 단위.**
- 지금: 모듈 명령의 수다. 같은 모듈이면 어느 기기에서나 같다.
- 의심: 컴파일러가 다른 코드를 내면 같은 소스가 다른 자리에서 `work`로 실패한다.
- 정할 것: 결정성의 단위가 모듈인지 소스인지.
7. **고정 한도.**
- 지금: 상태 32, 입력 32, 레코드 16, 레코드의 필드 16, 키별 컬렉션 1, 모듈의 코드 65,535 명령, 값을 가진 중첩 8.
- 의심: 구현의 숫자가 뜻이 됐다. "어떤 명세든"과 맞지 않는다(140).
8. **교체의 세부.**
- 이름으로 잇는 것은 남긴다.
- 수와 bool을 서로 옮기는 것 같은 규칙은 수의 모델이 정해진 뒤 다시 본다.
9. **HTTP와 JSON.**
- 경계의 어댑터로 남는다(하이브리드). 계약은 아니다.
- 보기를 GET으로, 입력을 POST로 옮기는 것은 표면의 하나다. 노드 사이의 기본은 링크다.
## 얼릴 후보와 다시 세울 것
**얼릴 후보(1.0):**
- step이 전함수이고, 원자적이고, 결정적이다.
- 시간은 입력이다.
- 보기는 커밋된 상태의 순수 함수다.
- 보이는 역사는 커밋의 앞부분이다.
- 전달은 순서대로 한 번이고, 전송 상태는 저장소에 산다.
- 한도는 결정적인 단위로 세고, 실패는 그 앱에서 멈춘다.
- 받아들인 값은 모든 길에서 같다.
- 교체는 이름으로 잇는다.
**다시 세울 것(1.0 전):**
- 값과 연산, 곧 계산의 언어
- 입력과 보기의 종류
- 커서, 인덱스, 문서
- 수의 모델
- 예산의 단위
- 고정 한도
원칙은 하나다. **의미는 일반적으로 두고, 특수화는 구현 아래로 내린다.** 묶음 실행기가 그 사례다. 루프의 모양을 알아보고 안에서
특수화했는데, 다섯 단계 동안 앱은 한 줄도 바뀌지 않았다(134–138). TPC-C를 빠르게 한 것(HASHED 표현, 한 번 훑는 집계)도 이미
구현 쪽의 결정이다.
## 착수 기준 (다음 일)
- **바꿀 결정.** 계산의 핵(값, 연산, 재귀, 바이트)을 어떤 모양으로 다시 세울지 정한다.
- **남은 질문.**
- 세상의 명세들이 aup에서 처음 부딪치는 곳은 어디인가?
- 일반적인 핵이 지금의 패턴 전용 명령만큼 빠를 수 있는가?
- **최소 확인.** [140](../research/140-spec-suite.md)의 명세 묶음과 탐침이다.
- **중단 기준.** 일반적인 핵으로 옮긴 뒤 은행 질의의 명령 수가 1%, TPC-C가 3%를 넘게 나빠지면 멈춘다. 그때는 그 특수화를 구현
아래로 내리는 길을 먼저 찾는다. 찾지 못하면 그 패턴은 핵에 남긴다.
|
