논리의 신전

이 신전을 알아 두면, "타입 검사가 통과한다"라는 말의 뜻이 조금 깊어져요. 타입은 명제이고, 타입이 붙은 값은 작은 증명이에요 — Note 타입의 값을 짜 맞출 수 있었다는 건, "이건 Note의 모양을 하고 있다"라는 명제에 증명이 붙었다는 뜻이에요.

타입은 실행 시점에는 사라져요(type erasure). 신전은 땅 위에 건물을 남기지 않아요 — 하지만 심사를 통과한 문서만 배에 오르니까, 바다 건너편에서 생기는 사고가 줄어요. 수학이 공학을 떠받치는 방식 중에서, 가장 조용한 모습일지도 몰라요.

볼거리

• 장경각의 타입은 Activity Vocabulary 명세에서 기계적으로 사경돼요 — "명세가 타입이 되고, 타입이 검사가 된다"라는 사경의 사슬이죠
• 타입 검사는 "그 모양이다"라는 것만 증명해요. "그 내용이 옳다"라는 건 증명하지 않아요 — 신전의 심사에도 관할이 있는 거죠
• 커리–하워드 대응을 끝까지 밀어붙인 증명 보조 시스템(Lean, Coq 등)에서는, 수학 정리 그 자체를 타입 검사로 확인해요. 이 신전의 총본산에 해당하죠

경문 한 구절

export default async function generateVocab(
  schemaDir: string,
  generatedPath: string,
): Promise<void> {
  const types = await loadSchemaFiles(schemaDir);
  const encoder = new TextEncoder();

  const file = await open(generatedPath, "w");
  const writer = file.createWriteStream();

  for await (const code of generateClasses(types)) {
    writer.write(encoder.encode(code));
  }