ChatGPT解决这个技术问题 Extra ChatGPT

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

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

我喜欢 Lisp 的自由格式宏,但我喜欢 Haskell 类型系统的健壮性。我很想看看静态类型的 Lisp 是什么样的。
好问题!我相信 shenlanguage.org 可以做到这一点。我希望它变得更加主流。
你如何使用 Haskell 进行符号计算? (解决'x'(=(+ xy)(* xy)))。如果你把它放在一个字符串中,就没有检查(不像 Lisp 可以使用宏来添加检查)。如果您使用代数数据类型或列表...它会非常冗长:solve (Sym "x") (Eq (Plus (Sym "x") (Sym "y")) (Mult (Sym "x") (符号“y”)))

E
Eli Barzilay

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


这里的问题是,构成类型化球拍程序的整个源代码的列表的类型是什么?
这通常是 Sexpr
但是,我可以用 eval 来写 coerce :: a->b。类型安全在哪里?
@ssice:当您使用像 eval 这样的无类型函数时,您需要测试结果以查看结果,这在 Typed Racked 中并不是什么新鲜事(与采用联合类型 StringNumber)。看到这个可以完成的一个隐含方式是,您可以在 HM 静态类型语言中编写和使用动态类型语言。
为什么标准的 HM 风格通常是 lisp 的错误选择?
O
Owen S.

如果你想要的只是一种看起来像 Lisp 的静态类型语言,你可以很容易地做到这一点,方法是定义一个代表你的语言的抽象语法树,然后将该 AST 映射到 S 表达式。但是,我认为我不会将结果称为 Lisp。

如果你想要一些除了语法之外实际上具有 Lisp-y 特征的东西,可以使用静态类型语言来做到这一点。然而,Lisp 有许多特性很难从中获得很多有用的静态类型。为了说明这一点,让我们看一下列表结构本身,称为 cons,它构成了 Lisp 的主要构建块。

尽管 (1 2 3) 看起来像一个列表,但将 cons 称为列表有点用词不当。例如,它根本无法与静态类型列表(如 C++ 的 std::list 或 Haskell 的列表)相提并论。这些是一维链表,其中所有单元格都属于同一类型。 Lisp 很高兴地允许 (1 "abc" #\d 'foo)。此外,即使您将静态类型列表扩展为涵盖列表列表,这些对象的类型也要求列表的 每个 元素都是子列表。您将如何在其中代表 ((1 2) 3 4)

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

那么,您将如何在静态类型语言中对这样的结构进行建模呢?让我们在 Haskell 中尝试一下,它具有极其强大和精确的静态类型系统:

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(即顶部)。

为了使用它们,你必须想出机制来动态地将原子的值强制到你可以实际使用的东西上。到那时,您基本上已经在静态类型语言中实现了一个动态类型子系统! (人们不禁注意到 Greenspun's Tenth Rule of Programming 的一个可能推论。)

请注意,Haskell 仅支持具有 Obj 类型的 dynamic subsystem,与 Dynamic 类型和 Typeable class 结合使用以替换我们的 Atomic 类,允许将任意值与其类型,以及从这些类型返回的显式强制。这就是你需要使用的那种系统来处理 Lisp cons 结构的全部通用性。

您还可以做的是另一种方式,在本质上是动态类型的语言中嵌入一个静态类型的子系统。这使您可以对可以利用更严格类型要求的程序部分进行静态类型检查。例如,这似乎是在 CMUCL 的有限形式 precise type checking 中采用的方法。

最后,有可能拥有两个独立的子系统,动态类型和静态类型,它们使用契约式编程来帮助导航两者之间的转换。这样,该语言就可以适应 Lisp 的使用,其中静态类型检查将是一个障碍而不是帮助,以及静态类型检查将是有利的用途。这是 Typed Racket 所采用的方法,您将从下面的评论中看到。


这个答案存在一个基本问题:您假设静态类型系统必须是 HM 样式的。在那里无法表达的基本概念是子类型,它是 Lisp 代码的一个重要特征。如果您看一下 typed racket,您会发现它可以轻松表达任何类型的列表,包括 (Listof Integer)(Listof Any) 之类的东西。显然,您会怀疑后者是无用的,因为您对类型一无所知,但在 TR 中,您稍后可以使用 (if (integer? x) ...),系统将知道 x 是第一个分支中的整数。
哦,这是对类型球拍的一个不好的描述(这与你在某些地方发现的不健全的类型系统不同)。 Typed Racket 是一种静态类型语言,没有类型代码的运行时开销。 Racket 仍然允许在 TR 中编写一些代码,而在通常的无类型语言中编写一些代码——对于这些情况,合同(动态检查)用于保护类型代码免受潜在行为不端的无类型代码的影响。
@Eli Barzilay:我撒谎了,有四个部分: 4. 有趣的是,行业接受的 C++ 编码风格如何逐渐从子类型转向泛型。弱点是该语言不提供帮助来声明泛型函数将要使用的接口,类型类当然可以提供帮助。另外,C++0x 可能会添加类型推断。不是HM,我想,而是朝那个方向爬行?
Owen:(1) 重点是你需要子类型来表达 lispers 编写的代码类型——而你不能在 HM 系统中拥有它,所以你不得不为每次使用自定义类型和构造函数,这使整个东西使用起来更加尴尬。在类型化球拍中,使用具有子类型的系统是有意设计决策的必然结果:结果应该能够表达此类代码的类型,而无需更改代码或创建自定义类型。
(2) 是的,dynamic 类型在静态语言中越来越流行,作为一种解决方法,以获得动态类型语言的一些好处,这些值的通常折衷以一种使类型生成的方式包装可识别的。但是在这里,too typed racket 在使语言中的便利性方面做得非常好——类型检查器使用谓词的出现来了解更多关于类型的信息。例如,请参阅 racket page 上的键入示例,并了解 string? 如何将字符串和数字列表“简化”为字符串列表。
G
Gian

我的回答,如果没有高度的自信,大概就是这样。例如,如果你看一下像 SML 这样的语言,并将它与 Lisp 进行比较,它们的功能核心几乎是相同的。因此,将某种静态类型应用于 Lisp 的核心(函数应用程序和原始值)似乎不会有太多麻烦。

不过,您的问题确实说得很完整,而我看到的一些问题是代码即数据方法。类型存在于比表达式更抽象的层次。 Lisp 没有这种区别——所有的东西在结构上都是“扁平的”。如果我们考虑某个表达式 E : T(其中 T 是其类型的某种表示),然后我们将此表达式视为普通的 ol' 数据,那么这里的 T 的类型到底是什么?嗯,是种! kind 是一种更高阶的类型,所以让我们继续在我们的代码中说明这一点:

E : T :: K

你可能会看到我要去哪里。我敢肯定,通过从代码中分离出类型信息,可以避免这种类型的自引用,但是这会使这些类型的风格不太“lisp”。可能有很多方法可以解决这个问题,尽管对我来说这不是最好的方法。

编辑:哦,所以通过谷歌搜索,我找到了 Qi,它似乎与 Lisp 非常相似,只是它是静态类型的。也许这是一个开始查看他们在哪里进行更改以获取静态类型的好地方。


Qi 之后的下一个迭代似乎是 Shen,由同一个人开发。
R
Rainer Joswig

迪伦:Extending Dylan's type system for better type inference and error detection


链接已失效。但无论如何,Dylan 不是静态类型的。
@BjörnLindqvist:该链接指向一篇关于向 Dylan 添加渐进式打字的论文。
@BjörnLindqvist:我链接到了一篇概述论文。
但渐进式打字不算作静态打字。如果是这样,那么 Pypy 将是静态类型的 Python,因为它也使用渐进类型。
@BjörnLindqvist:如果我们通过渐进类型添加静态类型并在编译期间检查这些类型,那么这就是静态类型。并不是整个程序都是静态类型的,而是部分/区域。 homes.sice.indiana.edu/jsiek/what-is-gradual-typing“渐进类型化是我在 2006 年与 Walid Taha 一起开发的类型系统,它允许程序的某些部分是动态类型的,而其他部分是静态类型的。”