静态类型的完整 Lisp 变体可能吗?

静态类型的完整 Lisp 变体可能吗?这种东西存在有意义吗?我相信 Lisp 语言的优点之一就是它的定义简单。静态类型会损害这一核心原则吗?

31788 次浏览

我的答案是,没有高度自信的 probably。例如,如果您查看 SML 这样的语言,并将其与 Lisp 进行比较,那么它们的函数核心几乎是相同的。因此,将某种静态类型应用到 Lisp 的核心(函数应用程序和原始值)似乎不会有太大的问题。

但是,您的问题确实提到了 满了,我认为一些问题出现在代码即数据方法上。类型存在于比表达式更抽象的级别。Lisp 没有这种区别——所有东西在结构上都是“扁平的”。如果我们考虑一个表达式 E: T (其中 T 是它的类型的一些表示) ,然后我们认为这个表达式是普通的 ol’数据,那么这里 T 的类型到底是什么?这是一种!A 是一个高阶类型,所以让我们继续在代码中讨论它:

E : T :: K

你可能会明白我的意思。我确信,通过将类型信息从代码中分离出来,可以避免类型的这种自引用,但是这会使类型的风格不太“ lisp”。可能有很多方法可以解决这个问题,尽管对我来说不是很明显,哪种方法是最好的。

编辑: 哦,所以我用谷歌搜索了一下,找到了 阿七,它看起来和 Lisp 非常相似,只是它是静态类型的。也许从这里开始查看他们在哪里进行了更改以获得静态类型是一个很好的开始。

是的,这是非常有可能的,尽管对于大多数惯用的 Lisp/Scheme 代码来说,标准的 HM 风格的类型系统通常是错误的选择。有关最近使用的具有静态类型的“ Full Lisp”(实际上更像 Scheme)语言,请参见 Typed Racket

If all you wanted was a statically typed language that 看起来像 Lisp, you could do that rather easily, by defining an abstract syntax tree that represents your language and then mapping that AST to S-expressions. However, I don't think I would call the result Lisp.

如果您希望除了语法之外还有其他具有 Lisp-y 特征的东西,那么可以使用静态类型语言来实现这一点。然而,Lisp 有许多特性很难从中得到有用的静态类型。为了说明这一点,让我们看一下列表结构本身,称为 缺点,它构成了 Lisp 的主要构建块。

Calling the cons a list, though (1 2 3) looks like one, is a bit of a misnomer. For example, it's not at all comparable to a statically typed list, like C++'s std::list or Haskell's list. Those are single-dimensional linked lists where all the cells are of the same type. Lisp happily allows (1 "abc" #\d 'foo). Plus, even if you extend your static-typed lists to cover lists-of-lists, the type of these objects requires that 每个 element of the list is a sublist. How would you represent ((1 2) 3 4) in them?

Lisp conses 形成一个二叉树,有叶子(原子)和分支(conses)。此外,这种树的叶子可能包含任何原子(非缺点) Lisp 类型!这种结构的灵活性使得 Lisp 非常擅长处理符号计算、 AST 和转换 Lisp 代码本身!

那么,如何在静态类型语言中建模这样的结构呢?让我们在哈斯克尔尝试一下,那里有一个非常强大和精确的静态类型系统:

type Symbol = String
data Atom = ASymbol Symbol | AInt Int | AString String | Nil
data Cons = CCons Cons Cons
| CAtom Atom

第一个问题是 Atom 类型的作用域。显然,我们还没有选择一种 Atom 类型的足够灵活性来覆盖我们希望在 conses 中悬挂的所有类型的对象。我们没有尝试扩展上面列出的 Atom 数据结构(您可以清楚地看到这种结构很脆弱) ,而是使用了一个神奇的类型类 Atomic来区分我们想要创建原子的所有类型。那么我们可以试试:

class Atomic a where ?????
data Atomic a => Cons a = CCons Cons Cons
| CAtom a

但是这不会起作用,因为它要求树中的所有原子都是 一样类型的。我们希望它们能够因叶而异。一种更好的方法需要使用 Haskell 的 存在量词存在量词:

class Atomic a where ?????
data Cons = CCons Cons Cons
| forall a. Atomic a => CAtom a

但现在你来到了问题的关键。在这种结构下,你能对原子做什么?它们有什么共同的结构可以用 Atomic a建模?这种类型能保证什么程度的类型安全?注意,我们没有在类型类中添加任何函数,这是有原因的: 原子在 Lisp 中没有任何共同之处。它们在 Lisp 中的超类型简称为 t(即 top)。

为了使用它们,您必须想出一些机制,使原子的值与您实际使用的值 动态胁迫成正比。此时,您基本上已经在您的静态类型语言中实现了一个动态类型子系统!(人们不得不注意到 格林斯潘编程的第十条规则的一个可能的推论。)

请注意,Haskell 提供了对 动态子系统动态子系统的支持,Obj类型与 Dynamic类型和 打字类结合使用来替换我们的 Atomic类,Atomic类允许将任意值与它们的类型一起存储,并从这些类型显式地强制返回。您需要使用这种系统来处理 Lisp con 结构的完整通用性。

您还可以采取另一种方式,将静态类型的子系统嵌入到本质上是动态类型的语言中。这使您可以利用程序中可以利用更严格类型要求的部分进行静态类型检查。例如,这似乎是 CMUCL 的有限形式的 精密型号检验精密型号检验所采取的方法。

最后,还可能有两个独立的子系统,动态类型和静态类型,它们使用契约式编程来帮助导航两者之间的转换。通过这种方式,该语言可以适应 Lisp 的使用,在这种情况下,静态类型检查更多地是一种障碍,而不是一种帮助,还可以适应静态类型检查更为有利的情况。这是 敲击键盘采用的方法,您将从下面的评论中看到。