luo*_*990 35 haskell coq agda dependent-type idris
我被告知在依赖类型系统中,"类型"和"值"是混合的,我们可以将它们都视为"术语".
但是有一些我无法理解的东西:在没有Dependent Type(如Haskell)的强类型编程语言中,在编译时决定(推理或检查)类型,但是在运行时决定(计算或输入)值.
我认为这两个阶段之间肯定存在差距.试想一下如果从STDIN以交互方式读取一个值,我们如何在必须决定AOT的类型中引用该值？
例如,我需要从STDIN中读取一个自然数n和一个自然数列表xs(包含n个元素),如何将它们放入数据结构中Vect n Nat？
chi*_*chi 43
假设我们n :: Int在运行时输入STDIN.然后我们读取n字符串,并将它们存储vn :: Vect n String(假装暂时可以完成).同样,我们可以阅读m :: Int和vm :: Vect m String.最后,我们连接两个向量:( vn ++ vm这里简化一点).这可以是类型检查,并将具有类型Vect (n+m) String.
现在确实,类型检查器在编译时运行,在值n,m已知之前运行,之前也是vn,vm已知的.但这并不重要:我们仍然可以象征性地对未知数进行推理,n,m并认为即使我们还不知道究竟是什么,也会vn ++ vm涉及这种类型.n+mn+m
它与数学没有什么不同,我们根据一些规则操纵涉及未知变量的符号表达式,即使我们不知道变量的值.我们不需要知道n看到的是什么号码n+n = 2*n.
同样,类型检查器可以键入检查
-- pseudocode
readNStrings :: (n :: Int) -> IO (Vect n String)
readNStrings O = return Vect.empty
readNStrings (S p) = do
s <- getLine
vp <- readNStrings p
return (Vect.cons s vp)
(好吧,实际上可能需要程序员提供一些帮助来进行类型检查,因为它涉及依赖匹配和递归.但我会忽略这一点.)
重要的是,类型检查器可以在不知道是什么的情况下检查n.
请注意,多态函数实际上已经出现了同样的问题.
fst :: forall a b. (a, b) -> a
fst (x, y) = x
test1 = fst @ Int @ Float (2, 3.5)
test2 = fst @ String @ Bool ("hi!", True)
...
人们可能想知道"如果fst不知道什么类型a并且b将在运行时,类型检查器如何检查？".再次,通过象征性的推理.
对于类型参数,这可以说是更明显的,因为我们通常在类型擦除之后运行程序,这与n :: Int上面的值参数不同,后者无法擦除.尽管如此,在普遍量化类型或类型之间存在一些相似之处Int.
在我看来，这里有两个问题：
鉴于某些值在编译时是未知的（例如，从 STDIN 读取的值），我们如何在类型中使用它们？（请注意，chi 已经对此给出了很好的答案。）
某些操作（例如，getLine）在编译时似乎完全没有意义；我们怎么可能用类型来谈论它们？
正如 chi 所说，(1) 的答案是象征性的或抽象的推理。您可以读入一个数字n，然后Vect n Nat通过从命令行读取n时间来构建一个过程，利用算术属性，例如1+(n-1) = n对于非零自然数的事实。
(2) 的答案有点微妙。天真，你可能要说“这个函数返回长的矢量n，其中n从命令行读”。您可能会尝试给出两种类型（如果我弄错了 Haskell 符号，我深表歉意）
unsafePerformIO (do n <- getLine; return (IO (Vect (read n :: Int) Nat)))
或（在伪 Coq 符号中，因为我不确定 Haskell 的存在类型符号是什么）
IO (exists n, Vect n Nat)
这两种类型实际上都可以理解，并且可以说不同的事情。对我来说，第一种类型是“在编译时，n从命令行读取，并返回一个函数，该函数在运行时n通过执行 IO给出长度向量”。第二种类型表示“在运行时，执行 IO 以获取自然数n和长度向量n”。
我喜欢看待这个问题的方式是所有的副作用（除了可能是非终止之外）都是 monad 转换器，并且只有一个 monad：“真实世界”的 monad。Monad 转换器在类型级别和术语级别都可以正常工作；特别的一件事是run :: M a -> a在“现实世界”中执行 monad（或 monad 转换器堆栈）。您可以在两个时间点调用run：一个是在编译时，您可以在该时间点调用run在类型级别显示的任何实例。另一个是在运行时，您可以在其中调用run在值级别显示的任何实例。注意run仅当您指定评估顺序时才有意义；如果您的语言未指定是按值调用还是按名称调用（或按推值调用或按需要调用或按其他方式调用），则可能会出现不一致你尝试计算一个类型。