../

// 类型级编程：一个最平凡的例子
#import "/template.typ": doc-template

#doc-template(
title: "类型级编程：一个最平凡的例子",
date: "2025年5月17日",
body: [

本文将使用Haskell。

起手先开一些扩展：

```
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds#-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Werror=incomplete-patterns #-}

import Data.Type.Equality
```

= 零一

计算机中的一切都是「零」和「一」：

```
data Bit = Zero | One
```

为Bit类型中的两个值：「零」和「一」，各自创建类型，是为单例类型（Singleton
Type）：

```
-- 前缀S，是Sing

...