把一个React应用迁移到Idris加Spock这套技术栈，听起来像是一次激进的重构，但实际操作下来你会发现，这更像是一次“把防御性代码搬进类型系统”的过程。React应用中大量的运行时校验逻辑，比如表单字段非空检查、数值范围检查、状态枚举合法性检查，在依赖类型的帮助下都可以变成编译期约束。也就是说，那些原本要靠if (x === undefined)一层层兜底的代码，直接写不出来才是常态。这篇文章会从类型系统的能力边界讲起，逐步拆解迁移思路，并给出可运行的Spock服务端代码。
依赖类型到底解决了TypeScript覆盖不到的什么问题
先说结论：TypeScript的类型系统可以表达“这个值是字符串”，但很难低成本地表达“这个字符串必须是非空的”、“这个数字必须在1到100之间”这类依赖于值的约束。当然，TS里有branded type、有模板字面量类型，能模拟一部分，但写起来繁琐，而且一旦需要表达更复杂的关系，比如“分页查询的pageSize不能超过totalCount”、“订单状态是已发货时必须有物流单号”，TS的表达力就开始吃力了。
Idris是全量依赖类型的语言，类型可以依赖值，值也可以出现在类型里。举个最经典的例子，非空列表不需要单独定义一个类型，直接用向量（Vector）就行：
-- Vect 是长度依赖在类型里的列表 -- Vect 3 String 表示恰好包含3个String的列表 record User where constructor MkUser username : String tags : Vect 2 String -- 恰好两个标签，长度写死在类型里
这段代码里Vect 2 String的含义是：这个字段必须恰好是两个字符串，一个不多一个不少。想塞进去三个元素？编译器直接报错。这不是运行时校验，是结构层面就不允许非法数据存在。React里等价的逻辑往往是一堆useEffect加断言，或者借助zod这样的库在运行时验证，两者在可靠性上完全不是一个量级。
再看一个更贴近Web开发的场景。假设你的React应用有一个创建订单的表单，业务规则是：金额必须为正数，且当支付方式为“货到付款”时必须填写收货时间段。用依赖类型可以把这条规则直接编码进类型：
data Payment = Online | COD
data Order : Payment -> Type where
MkOnlineOrder : (amount : Nat) -> Order Online
MkCODOrder : (amount : Nat)
-> (timeWindow : (String, String))
-> Order COD这样一来，Order COD类型的值必然携带时间段，Order Online则必然没有。你无法构造出一个“货到付款但没有时间窗”的订单，因为这样的构造函数根本不存在。这种“让非法状态不可表示”的设计哲学，就是迁移到Idris最大的收益来源。
React状态管理思路与类型驱动设计的对照
React组件的状态管理本质上是命令式的：你调用setState，UI响应变化，至于新状态是否合法，框架不管，只能靠开发者自觉或者外部校验库。而类型驱动开发（Type-Driven Development）的思路是反过来的：先把不变量写进类型，再让编译器逼着你写满足这些不变量的实现。
迁移时的实际操作可以分三步。第一步，把React应用中所有的运行时校验逻辑找出来，列成一张清单：字段非空、枚举取值、数值范围、跨字段依赖关系。第二步，把每一条规则翻译成类型定义，这一步通常是最费脑子的，因为你要思考的是“数据长什么样才算合法”，而不是“怎么在运行时拦截非法数据”。第三步，把展示逻辑留在前端（React可以继续用），把数据和业务逻辑下沉到Idris后端。
这里要澄清一个常见误解：迁移到Idris加Spock并不意味着你要扔掉React。实践中更务实的架构是，前端继续用React渲染界面，后端用Spock提供API，但接口的请求和响应类型全部由Idris类型系统保证。前端拿到的数据只要能通过JSON反序列化，就一定满足后端定义的所有业务约束，因为不满足的数据在服务器上根本构造不出来。这比在两边各写一套校验逻辑要省心得多。
跨字段依赖是收益最明显的部分。比如用户注册时，“企业用户必须填税号，个人用户不能填”这条规则，在React里通常是提交时校验再报错，用户填完一大堆信息才被打回。而类型驱动的做法是让前端根据用户类型动态切换表单结构，后端用两个不同的构造函数接收，提交一次就能成功，用户体验和代码可靠性同时提升。
用Spock搭建类型安全的HTTP接口
Spock是Idris生态里最常用的轻量Web框架，风格类似Haskell的Scotty，路由写法简洁，和Idris的类型系统配合得很自然。下面给一个完整可运行的服务器示例，包含路由定义、类型化的请求体处理和JSON响应。
先写包声明和导入：
module Main where import Control.Monad.IO.Class import Data.Aeson import Network.Wai.Handler.Warp (run) import Web.Spock import Web.Spock.Config
然后定义业务类型。注意这里的User要求用户名非空，我们用一个自定义的智能构造来保证：
-- 用户名长度至少为2，约束依赖在类型层面体现
data ValidatedUser : Type where
MkValidatedUser : (name : String)
-> {auto prf : LTE 2 (length name)}
-> ValidatedUser
data ApiError = ValidationError String
instance ToJSON ValidatedUser where
toJSON (MkValidatedUser name _) =
object ["name" .= name]{auto prf : LTE 2 (length name)}这个隐式参数的含义是：构造ValidatedUser时，编译器必须能自动找到“2小于等于name长度”的证明，找不到就编译失败。这就是依赖类型的精髓——约束是证明，证明由编译器搜索。
最后是Spock的主服务，跑在本地8080端口：
main : IO ()
main = do
cfg <- defaultSpockCfg () PCNoDatabase ()
runSpock 8080 (spock cfg app)
app : SpockAction () () () ()
-> ActionCtxT () IO ()
app = do
get "api" $ text "Idris Spock Server Running"
get ("api" <//> "user" <//> var) $ \userName -> do
if length userName >= 2
then json $ MkValidatedUser userName
else setStatus 400 >> json (ValidationError "用户名至少两个字符")这段代码跑起来之后，用浏览器访问127.0.0.1:8080/api就能看到响应。上面这个例子为了演示JSON输出，在路由里做了一次运行时判断，实际项目中更地道的做法是把JSON解析和验证统一放到一个“验证器”函数里，解析失败直接返回错误通道，成功则返回带证明的强类型值，后续所有处理函数的签名都只接受这个强类型，非法数据从入口就被挡住。
编译这个项目需要安装Idris2，然后配置spock包依赖，用idris2 --build pack.ipkg或者配合pack构建工具即可。初次接触Idris2的包管理可能会觉得生态不如npm丰富，这是事实，但核心的Web开发链路——路由、JSON序列化、数据库访问（通过idrissql相关库）——都是可用的。
迁移过程中的坑与务实建议
坦率地说，这套技术栈不适合所有项目。第一个现实问题是招聘和学习曲线：依赖类型要求开发者理解证明的基本概念，初期写代码会遇到“编译器要求我提供一个证明”的困惑，这是从命令式语言转过来最难适应的一点。第二个问题是生态成熟度，Idris2的HTTP中间件、ORM生态远不如Node.js丰富，遇到问题时Stack Overflow上的答案也少得多。
务实的迁移策略是增量式的。先挑一个内部管理工具或者数据校验密集的小模块试点，比如报表导出、批量数据导入这类对类型安全收益高、对UI交互要求低的功能。React前端保持不动，只是把对应的API从Node.js后端换成Spock后端，前端通过fetch调用，几乎无感知。跑通之后再评估是否扩大范围。
还有一个技巧值得分享：把Idris编译成一个独立的可执行文件作为微服务部署，而不是替换整个后端。这样它和现有的Node.js服务可以并存，通过内部HTTP通信。类型安全的边界清晰（就是这个服务的接口），迁移风险可控，团队也有时间逐步适应类型驱动的思维方式。等团队里有人开始主动用“让非法状态不可表示”来设计模块时，再考虑把核心业务逻辑整体迁移也不迟。