Yes, it's very possible, although a standard HM-style type system is usually the wrong choice for most idiomatic Lisp/Scheme code. See Typed Racket for a recent language that is a "Full Lisp" (more like Scheme, actually) with static typing.
type Symbol = String
data Atom = ASymbol Symbol | AInt Int | AString String | Nil
data Cons = CCons Cons Cons
| CAtom Atom
您的第一个问题将是 Atom 类型的范围。显然，我们没有选择足够灵活的 Atom 类型来涵盖我们想要在 conses 中使用的所有对象类型。假设我们有一个神奇的类型类 Atomic ，它可以区分我们想要原子化的所有类型，而不是尝试扩展上面列出的 Atom 数据结构（您可以清楚地看到它很脆弱）。然后我们可以尝试：
class Atomic a where ?????
data Atomic a => Cons a = CCons Cons Cons
| CAtom a
If all you wanted was a statically typed language that looked like 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.
If you want something that actually has Lisp-y characteristics besides the syntax, it's possible to do this with a statically typed language. However, there are many characteristics to Lisp that are difficult to get much useful static typing out of. To illustrate, let's take a look at the list structure itself, called the cons, which forms the primary building block of 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 every element of the list is a sublist. How would you represent ((1 2) 3 4) in them?
Lisp conses form a binary tree, with leaves (atoms) and branches (conses). Further, the leaves of such a tree may contain any atomic (non-cons) Lisp type at all! The flexibility of this structure is what makes Lisp so good at handling symbolic computation, ASTs, and transforming Lisp code itself!
So how would you model such a structure in a statically typed language? Let's try it in Haskell, which has an extremely powerful and precise static type system:
type Symbol = String
data Atom = ASymbol Symbol | AInt Int | AString String | Nil
data Cons = CCons Cons Cons
| CAtom Atom
Your first problem is going to be the scope of the Atom type. Clearly, we haven't picked an Atom type of sufficient flexibility to cover all the types of objects we want to sling around in conses. Instead of trying to extend the Atom data structure as listed above (which you can clearly see is brittle), let's say we had a magical type class Atomic that distinguished all the types we wanted to make atomic. Then we might try:
class Atomic a where ?????
data Atomic a => Cons a = CCons Cons Cons
| CAtom a
But this won't work because it requires all atoms in the tree to be of the same type. We want them to be able to differ from leaf to leaf. A better approach requires the use of Haskell's existential quantifiers:
class Atomic a where ?????
data Cons = CCons Cons Cons
| forall a. Atomic a => CAtom a
But now you come to the crux of the matter. What can you do with atoms in this kind of structure? What structure do they have in common that could be modeled with Atomic a? What level of type safety are you guaranteed with such a type? Note we haven't added any functions to our type class, and there's a good reason: the atoms share nothing in common in Lisp. Their supertype in Lisp is simply called t (i.e. top).
In order to use them, you'd have to come up with mechanisms to dynamically coerce the value of an atom to something you can actually use. And at that point, you've basically implemented a dynamically typed subsystem within your statically typed language! (One cannot help but note a possible corollary to Greenspun's Tenth Rule of Programming.)
Note that Haskell provides support for just such a dynamic subsystem with an Obj type, used in conjunction with a Dynamic type and a Typeable class to replace our Atomic class, that allow arbitrary values to be stored with their types, and explicit coercion back from those types. That's the kind of system you'd need to use to work with Lisp cons structures in their full generality.
What you can also do is go the other way, and embed a statically typed subsystem within an essentially dynamically typed language. This allows you the benefit of static type checking for the parts of your program that can take advantage of more stringent type requirements. This seems to be the approach taken in CMUCL's limited form of precise type checking, for example.
Finally, there's the possibility of having two separate subsystems, dynamically and statically typed, that use contract-style programming to help navigate the transition between the two. That way the language can accommodate usages of Lisp where static type checking would be more of a hindrance than a help, as well as uses where static type checking would be advantageous. This is the approach taken by Typed Racket, as you will see from the comments that follow.
不过，您的问题确实是完整，而且我看到一些问题来自于代码即数据方法。类型存在于比表达式更抽象的层次上。 Lisp 没有这种区别——一切在结构上都是“扁平”的。如果我们考虑某个表达式 E : T （其中 T 是其类型的某种表示），然后我们将该表达式视为普通数据，那么这里 T 的类型到底是什么？嗯，是一种！种类是一种更高的顺序类型，所以让我们继续在我们的代码中对此进行一些说明：
My answer, without a high degree of confidence is probably. If you look at a language like SML, for example, and compare it with Lisp, the functional core of each is almost identical. As a result, it doesn't seem like you would have much trouble applying some kind of static typing to the core of Lisp (function application and primitive values).
Your question does say full though, and where I see some of the problem coming in is the code-as-data approach. Types exist at a more abstract level than expressions. Lisp doesn't have this distinction - everything is "flat" in structure. If we consider some expression E : T (where T is some representation of its type), and then we consider this expression as being plain ol' data, then what exactly is the type of T here? Well, it's a kind! A kind is a higher, order type, so let's just go ahead and say something about that in our code:
E : T :: K
You might see where I'm going with this. I'm sure by separating out the type information from the code it would be possible to avoid this kind of self-referentiality of types, however that would make the types not very "lisp" in their flavour. There are probably many ways around this, though it's not obvious to me which would be the best one.
EDIT: Oh, so with a bit of googling, I found Qi, which appears to be very similar to Lisp except that it's statically typed. Perhaps it's a good place to start to see where they made changes to get the static typing in there.
发布评论
评论（4）
是的，这是很有可能的，尽管对于大多数惯用的 Lisp/Scheme 代码来说，标准 HM 风格的类型系统通常是错误的选择。请参阅 Typed Racket 了解最近出现的“Full Lisp”语言（更像是 Scheme） ，实际上）使用静态类型。
Yes, it's very possible, although a standard HM-style type system is usually the wrong choice for most idiomatic Lisp/Scheme code. See Typed Racket for a recent language that is a "Full Lisp" (more like Scheme, actually) with static typing.
如果您想要的只是一种看起来像 Lisp 的静态类型语言，那么您可以相当轻松地做到这一点，方法是定义代表您的语言的抽象语法树，然后将该 AST 映射到 S 表达式。然而，我不认为我会将结果称为 Lisp。
如果您想要除语法之外实际上具有 Lisp-y 特征的东西，可以使用静态类型语言来实现。然而，Lisp 有许多特性很难从中获得有用的静态类型。为了说明这一点，让我们看一下列表结构本身，称为 cons，它构成了 Lisp 的主要构建块。
尽管
(1 2 3)看起来像一个列表，但将缺点称为列表有点用词不当。例如，它根本无法与静态类型列表（例如 C++ 的 std::list 或 Haskell 列表）相比较。这些是一维链表，其中所有单元格都具有相同类型。 Lisp 很乐意允许(1 "abc" #\d 'foo)。另外，即使您扩展静态类型列表以覆盖列表列表，这些对象的类型也要求列表中的每个元素都是子列表。您将如何在其中表示((1 2) 3 4)？Lisp conses 形成一棵二叉树，具有叶子（原子）和分支（conses）。此外，这样一棵树的叶子可能包含任何原子（非 cons）Lisp 类型！这种结构的灵活性使得 Lisp 如此擅长处理符号计算、AST 和转换 Lisp 代码本身！
那么如何用静态类型语言对这样的结构进行建模呢？让我们在 Haskell 中尝试一下，它具有极其强大且精确的静态类型系统：
您的第一个问题将是 Atom 类型的范围。显然，我们没有选择足够灵活的 Atom 类型来涵盖我们想要在 conses 中使用的所有对象类型。假设我们有一个神奇的类型类
Atomic，它可以区分我们想要原子化的所有类型，而不是尝试扩展上面列出的 Atom 数据结构（您可以清楚地看到它很脆弱）。然后我们可以尝试：但这行不通，因为它要求树中的所有原子都具有相同类型。我们希望它们每片叶子都能有所不同。更好的方法需要使用 Haskell 的存在量词：
但现在你到达了问题的关键。你能用这种结构的原子做什么？它们有什么共同点可以用
Atomic a建模？这种类型能保证什么级别的类型安全？请注意，我们没有向类型类中添加任何函数，这是有充分理由的：原子在 Lisp 中没有任何共同点。它们在 Lisp 中的超类型简称为t（即 top）。为了使用它们，您必须想出一些机制来动态地将原子的值强制转换为您可以实际使用的值。到那时，您基本上已经在静态类型语言中实现了动态类型子系统！ （人们不禁注意到格林斯潘第十条编程规则的一个可能的推论。
） Haskell 提供了对这样的支持 具有
Obj类型的动态子系统，与Dynamic类型和 Typeable 类 来替换我们的Atomic类，允许任意值与其类型一起存储，并从这些类型显式强制返回。这就是你需要用来处理 Lisp cons 结构的完整通用性的系统。您还可以采取另一种方式，将静态类型子系统嵌入本质上动态类型的语言中。这使您能够受益于对程序部分进行静态类型检查，从而利用更严格的类型要求。这似乎是 CMUCL 的有限形式所采取的方法 精确例如，类型检查。
最后，有可能拥有两个独立的子系统（动态类型和静态类型），它们使用契约式编程来帮助导航两者之间的转换。这样，该语言就可以适应 Lisp 的使用，其中静态类型检查更多的是一种障碍而不是帮助，也可以适应静态类型检查有利的情况。这是 Typed Racket 所采用的方法，您将从以下评论。
If all you wanted was a statically typed language that looked like 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.
If you want something that actually has Lisp-y characteristics besides the syntax, it's possible to do this with a statically typed language. However, there are many characteristics to Lisp that are difficult to get much useful static typing out of. To illustrate, let's take a look at the list structure itself, called the cons, which forms the primary building block of 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++'sstd::listor 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 every element of the list is a sublist. How would you represent((1 2) 3 4)in them?Lisp conses form a binary tree, with leaves (atoms) and branches (conses). Further, the leaves of such a tree may contain any atomic (non-cons) Lisp type at all! The flexibility of this structure is what makes Lisp so good at handling symbolic computation, ASTs, and transforming Lisp code itself!
So how would you model such a structure in a statically typed language? Let's try it in Haskell, which has an extremely powerful and precise static type system:
Your first problem is going to be the scope of the Atom type. Clearly, we haven't picked an Atom type of sufficient flexibility to cover all the types of objects we want to sling around in conses. Instead of trying to extend the Atom data structure as listed above (which you can clearly see is brittle), let's say we had a magical type class
Atomicthat distinguished all the types we wanted to make atomic. Then we might try:But this won't work because it requires all atoms in the tree to be of the same type. We want them to be able to differ from leaf to leaf. A better approach requires the use of Haskell's existential quantifiers:
But now you come to the crux of the matter. What can you do with atoms in this kind of structure? What structure do they have in common that could be modeled with
Atomic a? What level of type safety are you guaranteed with such a type? Note we haven't added any functions to our type class, and there's a good reason: the atoms share nothing in common in Lisp. Their supertype in Lisp is simply calledt(i.e. top).In order to use them, you'd have to come up with mechanisms to dynamically coerce the value of an atom to something you can actually use. And at that point, you've basically implemented a dynamically typed subsystem within your statically typed language! (One cannot help but note a possible corollary to Greenspun's Tenth Rule of Programming.)
Note that Haskell provides support for just such a dynamic subsystem with an
Objtype, used in conjunction with aDynamictype and a Typeable class to replace ourAtomicclass, that allow arbitrary values to be stored with their types, and explicit coercion back from those types. That's the kind of system you'd need to use to work with Lisp cons structures in their full generality.What you can also do is go the other way, and embed a statically typed subsystem within an essentially dynamically typed language. This allows you the benefit of static type checking for the parts of your program that can take advantage of more stringent type requirements. This seems to be the approach taken in CMUCL's limited form of precise type checking, for example.
Finally, there's the possibility of having two separate subsystems, dynamically and statically typed, that use contract-style programming to help navigate the transition between the two. That way the language can accommodate usages of Lisp where static type checking would be more of a hindrance than a help, as well as uses where static type checking would be advantageous. This is the approach taken by Typed Racket, as you will see from the comments that follow.
如果没有高度的信心，我的回答是可能。例如，如果您查看像 SML 这样的语言，并将其与 Lisp 进行比较，就会发现两者的功能核心几乎相同。因此，将某种静态类型应用到 Lisp 的核心（函数应用和原始值）似乎不会遇到太大麻烦。
不过，您的问题确实是完整，而且我看到一些问题来自于代码即数据方法。类型存在于比表达式更抽象的层次上。 Lisp 没有这种区别——一切在结构上都是“扁平”的。如果我们考虑某个表达式 E : T （其中 T 是其类型的某种表示），然后我们将该表达式视为普通数据，那么这里 T 的类型到底是什么？嗯，是一种！种类是一种更高的顺序类型，所以让我们继续在我们的代码中对此进行一些说明：
您可能会明白我要说的是什么。我确信通过将类型信息从代码中分离出来，可以避免这种类型的自引用，但是这会使类型的风格变得不太“口齿不清”。可能有很多方法可以解决这个问题，尽管我不清楚哪一种是最好的。
编辑：哦，所以通过一些谷歌搜索，我发现 Qi ，它似乎与 Lisp 非常相似，只是它是静态类型的。也许这是一个开始查看他们在哪里进行更改以获取静态类型的好地方。
My answer, without a high degree of confidence is probably. If you look at a language like SML, for example, and compare it with Lisp, the functional core of each is almost identical. As a result, it doesn't seem like you would have much trouble applying some kind of static typing to the core of Lisp (function application and primitive values).
Your question does say full though, and where I see some of the problem coming in is the code-as-data approach. Types exist at a more abstract level than expressions. Lisp doesn't have this distinction - everything is "flat" in structure. If we consider some expression E : T (where T is some representation of its type), and then we consider this expression as being plain ol' data, then what exactly is the type of T here? Well, it's a kind! A kind is a higher, order type, so let's just go ahead and say something about that in our code:
You might see where I'm going with this. I'm sure by separating out the type information from the code it would be possible to avoid this kind of self-referentiality of types, however that would make the types not very "lisp" in their flavour. There are probably many ways around this, though it's not obvious to me which would be the best one.
EDIT: Oh, so with a bit of googling, I found Qi, which appears to be very similar to Lisp except that it's statically typed. Perhaps it's a good place to start to see where they made changes to get the static typing in there.
Dylan：扩展 Dylan 的类型系统为了更好的类型推断和错误检测
Dylan: Extending Dylan's type system for better type inference and error detection