为什么静态语言如此复杂?

2022 年 2 月 1 日 CSDN


作者 | hirrolot   译者 | 弯月

出品 | CSDN(ID:CSDNnews)

编程语言设计人员都在努力让自己的语言变得更加出色,拥有强类型系统,通过避免软件中的代码重复来减轻开发人员的工作量。然而,随着编程语言越来越出色,语言中渗透的重复性也越来越多。

我称之为“静态与动态二元性”:编程语言中引入的每一个新抽象,有可能是静态级别,也有可能是动态级别,甚至是二者兼具。在前两种情况下,抽象仅位于一个特定级别,语言中就会出现不一致;而在最后一种情况下,语言将不可避免地引入特征二元性。

在这里,“静态级别”指的是编译时的语言机制;而“动态级别”指的是在运行时执行代码。因此,常见的控制流运算符,例如if/while/for/return、数据结构和过程都是动态的,而静态类型系统的功能和语法宏则都是静态的。本质上,大多数静态语言抽象在动态空间中都有相对应的抽象,反之亦然:

下面,在进一步阐述该问题之前,让我先来演示一下如何使用静态和动态两种方法来实现逻辑上等价的程序。下面的大多数示例都是用 Rust 编写的,但任何其他足以表现类型系统的通用编程语言也同样可以。请记住,本文内容与编程语言无关,我们关注的是一般编程语言通用理念。


记录类型 - 数组

 

考虑日常工作需要使用的记录类型:

automobile-static.rs
structAutomobile { wheels: u8, seats: u8, manufacturer: String,}
fnmain() { let my_car = Automobile { wheels: 4, seats: 4, manufacturer:String::from("X"), };
println!( "My car has {} wheels and {}seats, and it was made by {}.", my_car.wheels, my_car.seats, my_car.manufacturer );}

这段代码也可以用数组实现:

automobile-dynamic.rsusestd::any::Any;#[repr(usize)]enumMyCar {    Wheels,    Seats,    Manufacturer,}fnmain() {    let my_car: [Box<dyn Any>; 3] =[Box::new(4), Box::new(4), Box::new("X")];    println!(        "My car has {} wheels and {}seats, and it was made by {}.",        my_car[MyCar::Wheels as usize]            .downcast_ref::<i32>()            .unwrap(),        my_car[MyCar::Seats asusize].downcast_ref::<i32>().unwrap(),        my_car[MyCar::Manufacturer as usize]            .downcast_ref::<&'staticstr>()            .unwrap()    );}

在上述代码中,如果为.downcast_ref 指定的类型不正确,就会出问题。但是程序的逻辑保持不变,只是类型检查会推迟到运行时。

我们可以更进一步,将静态的 Automobile 编码为异构列表:

automobile-hlist.rsusefrunk::{hlist, HList};structWheels(u8);structSeats(u8);structManufacturer(String);typeAutomobile = HList![Wheels, Seats, Manufacturer];fnmain() {    let my_car: Automobile = hlist![Wheels(4),Seats(4), Manufacturer(String::from("X"))];    println!(        "My car has {} wheels and {}seats, and it was made by {}.",        my_car.get::<Wheels, _>().0,        my_car.get::<Seats, _>().0,        my_car.get::<Manufacturer, _>().0    );}

这个版本强制执行的类型检查与 automobile-static.rs 完全一样,只不过还提供了使用普通集合操作type Automobile 的方法。例如,我们可以翻转 automobile:

assert_eq!( my_car.into_reverse(), hlist![Manufacturer(String::from("X")), Seats(4), Wheels(4)]);

或者可以把两辆汽车的数据zip到一起:

lettheir_car = hlist![Wheels(6), Seats(4),Manufacturer(String::from("Y"))];
assert_eq!( my_car.zip(their_car), hlist![ (Wheels(4), Wheels(6)), (Seats(4), Seats(4)), (Manufacturer(String::from("X")),Manufacturer(String::from("Y"))) ]);

等等。

然而,有时我们希望将类型级别的计算应用于普通的struct和enum上,但我们做不到,因为我们无法通过类型名称从相应的类型定义中提取其结构,尤其是当类型来自于crate之外时,我们没办法在上面添加派生宏。

为了解决这个问题,我们决定创建这样一个过程宏,通过实现一个通用 trait 来检查类型定义。这个通用 trait 拥有关联类型 type Repr,其实现等同于某种形式的可操作异构列表。尽管如此,由于上述 Rust的限制,所有其他没有此派生宏的类型就没法检查了。


和类型 - 树

 

我发现和类型特别适合表示抽象语法树的节点:

ast-static.rsusestd::ops::Deref;enumExpr {    Const(i32),    Add(Box<Expr>, Box<Expr>),    Sub(Box<Expr>, Box<Expr>),    Mul(Box<Expr>, Box<Expr>),    Div(Box<Expr>, Box<Expr>),}useExpr::*;fneval(expr: &Box<Expr>) -> i32 {    match expr.deref() {        Const(x) => *x,        Add(lhs, rhs) => eval(&lhs) +eval(&rhs),        Sub(lhs, rhs) => eval(&lhs) -eval(&rhs),        Mul(lhs, rhs) => eval(&lhs) *eval(&rhs),        Div(lhs, rhs) => eval(&lhs) /eval(&rhs),    }}fnmain() {    let expr: Expr = Add(        Const(53).into(),        Sub(            Div(Const(155).into(),Const(5).into()).into(),            Const(113).into(),        )        .into(),    );    println!("{}",eval(&expr.into()));}

同样也可以表示带标签的树:

ast-dynamic.rsusestd::any::Any;structTree {    tag: i32,    value: Box<dyn Any>,    nodes: Vec<Box<Tree>>,}constAST_TAG_CONST: i32 = 0;constAST_TAG_ADD: i32 = 1;constAST_TAG_SUB: i32 = 2;constAST_TAG_MUL: i32 = 3;constAST_TAG_DIV: i32 = 4;fneval(expr: &Tree) -> i32 {    let lhs = expr.nodes.get(0);    let rhs = expr.nodes.get(1);    match expr.tag {        AST_TAG_CONST =>*expr.value.downcast_ref::<i32>().unwrap(),        AST_TAG_ADD =>eval(&lhs.unwrap()) + eval(&rhs.unwrap()),        AST_TAG_SUB => eval(&lhs.unwrap())- eval(&rhs.unwrap()),        AST_TAG_MUL =>eval(&lhs.unwrap()) * eval(&rhs.unwrap()),        AST_TAG_DIV =>eval(&lhs.unwrap()) / eval(&rhs.unwrap()),        _ => panic!("Out ofrange"),    }}fnmain() {    let expr = /* Construction omitted... */;    println!("{}", eval(&expr));}

与上述 structAutomobile 的处理相同,我们也可以将 enum Expr 表示为 frunk::Coproduct。这项练习就留给读者了。


值 - 关联类型

 

我们想使用标准运算符! 来执行布尔值的非运算:

negate-dynamic.rs
fnmain() { assert_eq!(!true, false); assert_eq!(!false, true);}

我们可以使用关联类型来进行相同的处理:

negate-static.rsusestd::marker::PhantomData;traitBool {    type Value;}structTrue;structFalse;implBool for True { type Value = True; }implBool for False { type Value = False; }structNegate<Cond>(PhantomData<Cond>);implBool for Negate<True> {    type Value = False;}implBool for Negate<False> {    type Value = True;}constThisIsFalse: <Negate<True> as Bool>::Value = False;constThisIsTrue: <Negate<False> as Bool>::Value = True;

事实上,Rust 类型系统的图灵完备性正是建立在这一原则和类型归纳上。在 Rust 中看到一个普通值时,你都应该知道从计算的角度来看,它在类型的级别上都有正式的对应形式。每当你编写算法时,值在类型级别上都有对应的形式,并且使用概念上等价的构建方法!


递归 - 类型级别的归纳

 

让我再举一个例子:

peano-dynamic.rsusestd::ops::Deref;#[derive(Clone,Debug, PartialEq)]enumNat {    Z,    S(Box<Nat>),}fnadd(lhs: &Box<Nat>, rhs: &Box<Nat>) -> Nat {    match lhs.deref() {        Nat::Z => rhs.deref().clone(), // I        Nat::S(next) =>Nat::S(Box::new(add(next, rhs))), // II    }}fnmain() {    let one = Nat::S(Nat::Z.into());    let two = Nat::S(one.clone().into());    let three = Nat::S(two.clone().into());    assert_eq!(add(&one.into(),&two.into()), three);}

上述代码是自然数的皮亚诺编码。我们在 add 函数使用了递归来计算总和,并通过模式匹配判断何时停止。

由于递归对应于类型归纳,模式匹配对应于多实现,所以相同的处理也可以放到编译时:

peano-static.rsusestd::marker::PhantomData;structZ;structS<Next>(PhantomData<Next>);traitAdd<Rhs> {    type Result;}//Iimpl<Rhs>Add<Rhs> for Z {    type Result = Rhs;}//IIimpl<Lhs:Add<Rhs>, Rhs> Add<Rhs> for S<Lhs> {    type Result = S<<Lhs as Add<Rhs>>::Result>;}typeOne = S<Z>;typeTwo = S<One>;typeThree = S<Two>;constTHREE: <One as Add<Two>>::Result = S(PhantomData);

在这里,impl... for Z 是基本情况(终止情况),而 impl ... for S<Lhs> 是归纳步骤(递归情况),这很像match语句的模式匹配处理。与第一个示例一样,归纳首先将第一个参数归约成 Z:<Lhs as Add<Rhs>>::Result,实际的处理与 add(next,rhs) 一样,它会再次调用模式匹配,以实施进一步的计算。注意,这两个 trait 实现都属于同一个逻辑函数实现,虽然看起来不同,因为模式匹配针对的是类型级别上的数字(Z 和 S<Next>)。这有点类似于 Haskell,每个模式匹配看起来都像一个单独的函数定义:

peano-static.hsimportControl.ExceptiondataNat = Z | S Nat deriving Eqadd:: Nat -> Nat -> NataddZ rhs = rhs -- Iadd(S next) rhs = S(add next rhs) -- IIone= S Ztwo= S onethree= S twomain:: IO ()main= assert ((add one two) == three) $ pure (


类型级别逻辑的例子

 

本文的目的是探讨静态与动态二元性。如果想要静态与动态的转换库,则可以参考 type-operators(https://crates.io/crates/type-operators)。这其实是一个算法宏 eDSL,通过 trait 实现类型级别的操作,你可以定义代数数据类型,然后执行数据操作,类似于常见的 Rust 处理,只不过整个代码仍停留在类型级别。还有一个值得参考的项目是Fortraith(https://github.com/Ashymad/fortraith),它是一款编译时编译器,可以将 Forth 编译为编译时 trait 表达式:

forth!( : factorial (n -- n) 1 swap fact0 ; : fact0 (n n -- n) dup 1 = if drop else duprot * swap pred fact0 then ; 5 factorial .);

如上代码将一个简单的阶乘实现转换为 trait 和相关类型的计算。得到的结果如下:

println!(    "{}",    <<<Empty as five>::Result asfactorial>::Result as top>::Result::eval());

通过上述讨论可以看出,无论是静态类型还是动态类型,逻辑部分都保持不变,


静态类型的缺点

 

如今的编程语言都不关心逻辑,而是专注于底层的机制。他们认为将布尔的非操作是最基本的操作符,但有人认为 negative trait bounds仍然存在很多问题。大多数主流编程语言的标准库都支持树的数据结构,但几十年来仍然没有实现 sum 类型。我无法想象没有 if 运算符的编程语言,但只有个别编程语言完全支持 trait bound,更不要说模式匹配了。

这种不一致性导致软件工程师设计出低质量的API,有些 API 选择了动态类型以及寥寥几个编译时检查,而有些则选择了静态,并试图规避宿主语言的基本限制,从而导致这些 API 的使用越来越复杂。在一个解决方案中结合静态类型与动态类型非常困难,因为无法在静态上下文中调用动态类型。如果用颜色来做类比,那么动态即为红色,静态则为蓝色。

除了这种不一致性,我们还要面对特征二元性。在 C++、Haskell 和 Rust 等语言中,这种二元性是最反常的形式。你可以将所谓的“富有表现力”的编程语言视为两种或多种小语言的结合,比如 C++ 与C++ 模板/宏,Rust 与类型级别的 Rust + 声明性宏等。

如果采用这种方式,则每次编写的元级别的代码就不能在宿主语言中重用了,反之亦然,因此违反了 DRY 原则(即“一次且仅一次”原则)。此外,二元性增加了学习的难度,加剧了语言发展的难度,最终会导致功能膨胀,以至于只有作者才清楚代码在干什么。Haskell 的代码中包含大量的 GHC #LANGUAGE 子句,每个子句都表示一个单独的语言扩展:

feature-bloat.hs
{-#LANGUAGE BangPatterns #-}{-#LANGUAGE CPP #-}{-#LANGUAGE ConstraintKinds #-}{-#LANGUAGE DefaultSignatures #-}{-#LANGUAGE DeriveAnyClass #-}{-#LANGUAGE DeriveGeneric #-}{-#LANGUAGE DerivingStrategies #-}{-#LANGUAGE FlexibleContexts #-}{-#LANGUAGE FlexibleInstances #-}{-#LANGUAGE GADTs #-}{-#LANGUAGE GeneralizedNewtypeDeriving #-}{-#LANGUAGE NamedFieldPuns #-}{-#LANGUAGE OverloadedStrings #-}{-#LANGUAGE PolyKinds #-}{-#LANGUAGE RecordWildCards #-}{-#LANGUAGE ScopedTypeVariables #-}{-#LANGUAGE TypeFamilies #-}{-#LANGUAGE UndecidableInstances #-}{-#LANGUAGE ViewPatterns #-}

—— 摘自haskell/haskell-language-server(https://github.com/haskell/haskell-language-server/blob/ee0a0cc78352c961f641443eea89a26b9e1d3974/hls-plugin-api/src/Ide/Types.hs)

当宿主语言没有提供开发所需的静态功能时,一些程序员就会放飞自我,在现有的基础上创建全新的编译时元语言和 eDSL。因此,不一致性就有转化为二元性的危险:

●       C++:我们有模板元编程库,例如 Boost/Hana 和 Boost/MPL,二者都是在元级别使用类似 C++ 的功能:

take_while.cpp
BOOST_HANA_CONSTANT_CHECK( hana::take_while(hana::tuple_c<int, 0, 1, 2, 3>,hana::less.than(2_c)) == hana::tuple_c<int,0, 1>);

—— 摘自hana/example/take_while.cpp(https://github.com/boostorg/hana/blob/998033e9dba8c82e3c9496c274a3ad1acf4a2f36/example/take_while.cpp)

filter.cpp
constexpr auto is_integral = hana::compose(hana::trait<std::is_integral>, hana::typeid_);
static_assert( hana::filter(hana::make_tuple(1, 2.0, 3, 4.0), is_integral) == hana::make_tuple(1,3), "");static_assert( hana::filter(hana::just(3), is_integral) == hana::just(3),"");BOOST_HANA_CONSTANT_CHECK( hana::filter(hana::just(3.0), is_integral) == hana::nothing);

—— 摘自hana/example/filter.cpp(https://github.com/boostorg/hana/blob/998033e9dba8c82e3c9496c274a3ad1acf4a2f36/example/filter.cpp)

iter_fold.cpptypedef vector_c<int, 5, -1, 0, 7, 2, 0, -5, 4> numbers;typedef iter_fold<    numbers,   begin<numbers>::type,   if_<less<deref<_1>, deref<_2>>, _2, _1>>::type max_element_iter;BOOST_MPL_ASSERT_RELATION(   deref<max_element_iter>::type::value, ==, 7);

—— 摘自 thedocs of MPL(https://www.boost.org/doc/libs/1_78_0/libs/mpl/doc/refmanual/iter-fold.html)

  • C 语言:我自己写了一个编译时元编程框架 Metalang99,使用 C 预处理器实现了相同的功能。我结合了类似于 Lisp 的 trampoline 和连续传递样式技术,重新实现了递归。最后,我的标准库中构建了一堆列表操作函数,例如 ML99_listMap、ML99_listIntersperse 和 ML99_listFoldr,它们将  Metalang99 变成了纯粹的数据转换语言,比 C 本身更具表现力。

  • Rust:在本文的第一个不一致性示例中(Automobile),我们使用了 Frunk 库的异构列表。不难看出,Frunk 复制了集合和迭代器的一些功能,只是为了将它们提升到类型级别。虽然将Iterator::map 或 Iterator::intersperse 应用到异构列表听上去很酷,但我们实现不了。更糟糕的是,如果我们仍然想要执行声明性类型级别的数据转换,就必须保持迭代器适配器和类型级别的适配器之间的一一对应,每次为迭代器实现一个新的工具函数,就需要在 hlist 中也添加一个。

  • Rust:Typenum 也是一个流行的类型级别的库,它允许在编译时执行整数计算,它将整数编码成了泛型。在这种实现中,编程语言中的整数处理都有对应的静态处理,也因此引入了更多二元性。我们不能在参数中传递一些类型,比如 (2 + 2) * 5,我们必须写成:<<P2 asAdd<P2>>::Output as Mul<P5>>::Output。为此,最好的办法是编写一个宏来完成这些繁琐的工作,但它只是语法糖,无论如何你都会在编译时错误中看到上述 trait。

有时,软件工程师发现他们的语言过于原始,甚至无法通过动态代码表达他们的想法。但他们并没有放弃:

  • Golang:Kubernetes是最大的 Golang 代码库之一,其运行时包中实现了自己的面向对象类型系统。

  • C:VLC 媒体播放器有一个基于宏的插件 API,用于表示媒体编解码器。Opus 的定义方法请见这里(https://github.com/videolan/vlc/blob/271d3552b7ad097d796bc431e946931abbe15658/modules/codec/opus.c#L57)。

  • C:QEMU 模拟器建立在自定义对象模型之上:QObject、QNum、QNull、QList、QString、QDict、QBool 等。

回想一下著名的“格林斯潘第十定律”,这类自定义的元语言通常都是临时的、非正式指定的、漏洞百出,且速度很慢,不仅语义模糊,而且文档也很糟糕。元语言抽象的概念本身就不成立,尽管创建高度声明性的、小众特定领域语言乍一看听起来很酷。

在使用宿主语言表达某个问题领域时,你需要了解如何完成一系列的调用,也就是我们常说的 API;然而,如果 API 是用另一种语言编写的,那么除了调用顺序之外,还需要了解该语言的语法和语义,这就会产生问题,原因有两个:给开发人员带来思想上的负担,而且掌握了此类元语言的开发人员数量有限。

根据我的经验,自定义的元语言往往会很快失控,并殃及整个代码库,加剧深入理解的难度。不仅理解代码会受到影响,而且编译器与开发人员的交互也会受到影响,你有没有使用复杂的类型或宏 API 的经历?如果有,那么应该非常熟悉晦涩难懂的编译器诊断结果,就像下面的截图一样:

说起来很可悲,但如今说一门语言“富有表现力”,就等于是在说该语言的功能过于庞大,异常复杂。

最后,必须说一下宿主语言的元编程。对于 Template Haskell 和 Rust 过程宏这类的模板系统,我们可以使用相同的语言来操作宿主语言的抽象语法树,虽然没有二元性的问题,但编程语言常见的功能却不如人意。

宏不是函数,代码不能一部分使用宏,一部分使用函数,因为二者是不同的概念,因此我们很难设计一个既通用又简单的 API 库。我个人认为,Rust 过程宏在设计上是一个巨大的错误,而 C 语言的 #define 也是半斤八两,除了纯语法之外,宏系统根本不知道操作的语言。

这种方式根本无法优雅地扩展和使用语言,充其量不过是稍微好一点的文本替换。例如,假设有一个名为 Either 的枚举,其定义如下:

either.rs
pubenum Either<L, R> { Left(L), Right(R),}

现在假设有一个trait foo,我们希望为 Either<L, R> 实现这个 trait,而 L 和 R 都实现了 Foo。似乎我们并不能给 Either 应用一个实现了该 trait 的派生宏,即使知道名字也不行,因为这样做的话,宏就必须了解 Foo 的完整签名。更糟糕的是,Foo 可能是在其他库中定义的,意味着没有额外的元信息,就无从获知其定义。

尽管这个情况看上去很不常见,但事实却并非如此。我强烈建议你看看 tokio-util 中的 Either,它就是这种枚举,但它实现了 Tokio 专用的 traits,如AsyncRead、AsyncWrite、AsyncSeek 等。现在想象一下,你的项目中有五个不同的 Either,分别来自不同的库,那么集成就会非常麻烦!虽然类型内省也许是个这种方案,但不可避免地让本已复杂的语言雪上加霜。


Idris可以解决问题吗?

 

Idris 最根本的特性之一就是,类型和表达式都是用同一种语言表达的,它们的语法完全相同。

——Edwin Brady,Idris作者

我们来思考一下如何解决这个问题。如果采用完全动态的语言,就能解决二元性和不一致的问题,但会失去编译时验证,而且调试程序也会异常麻烦。动态类型系统的问题早已天下皆知。

解决问题的唯一方法就是让一门语言同时支持动态和静态,并且不要把同一个特性分成动态和静态两部分。因此,理想的语言抽象是动态的也是静态的;但是,它仍然是一个概念,而不是逻辑上相似但接口不同的两个概念。

一个很好的例子就是 CTFE,也就是 constexpr:同一段代码可以在编译时的静态上下文中执行,也可以在运行时的动态上下文中执行(例如通过 stdin 请求用户输入时)。因此,我们不需要为编译时(静态)和运行时(动态)编写不同的代码,只需要使用相同的表示即可。

我见过一种解决方案就是依赖类型。使用依赖类型,类型的参数不仅可以是其他类型,还可以是值。Idris 就是一种依赖类型语言,它有一种名为 Type 的类型,表示“所有类型的类型”,因此模糊了类型级别和值级别之间的界限。有了如此强大的工具,我们就可以表示有类型的抽象,而在一般语言中,这只能通过编译器或宏来实现。也许最常见、最有描述性的例子就是类型安全的 printf,它能即时计算参数的类型。

首先,定义一个可归纳的类型 Fmt,还有一个从格式字符串获取该类型的方法:

data Fmt= FArg Fmt | FChar Char Fmt | FEnd
toFmt : (fmt :List Char)-> FmttoFmt('*' ::xs) = FArg(toFmt xs)toFmt( x ::xs) = FCharx (toFmt xs)toFmt[] = FEnd

然后,使用它为printf 函数生成类型。为便于读者理解,语法参考了 Haskell。

下面是最有趣的部分:

PrintfType : (fmt : Fmt) -> TypePrintfType (FArgfmt) = ({ty :Type} ->Show ty =>(obj : ty) ->PrintfType fmt)PrintfType (FChar _ fmt) = PrintfType fmtPrintfType FEnd = String

这个函数做了什么?它根据输入参数 fmt 计算出了一个类型。像往常一样,我们将 fmt 分为三种情况,分别处理:

1、(FArg     fmt)。由于 FArg 表示我们要提供一个可打印的参数,在这个例子中会产生一个类型签名,要求一个额外的参数:

  1. {ty:Type}      的意思是 Idris 能够自动推断该参数的类型 ty(隐含参数)

  2. Show      ty 是一个类型约束,指明 ty 应当实现 Show。

  3. (obj:      ty) 是我们要提供给 printf 的可打印参数。

  4. PrintfType      fmt 是一个递归调用,负责处理输入 fmt 的剩余部分。在 Idris 中,可归纳类型由可归纳函数负责管理!

2、(FChar     _ fmt)。FChar 表示格式字符串中的一个普通字符,因此我们忽略它,继续看PrintfType     fmt。

3、FEnd。这是输入的结尾。因为我们需要 print 产生一个 String,我们返回 String 普通类型。

现在,假设格式字符串为"*x*",或者说 FArg (FChar ('x' (FArgFEnd)))。那么 PrintfType 会生成什么类型?很简单:

1、FArg: {ty : Type} -> Show ty =>     (obj : ty) -> PrintfType (FChar ('x' (FArg FEnd)))

2、FChar: {ty : Type} -> Show ty =>     (obj : ty) -> PrintfType (FArg FEnd)

3、FArg: {ty : Type} -> Show ty =>     (obj : ty) -> {ty : Type} -> Show ty => (obj : ty) ->     PrintfType FEnd

4、FEnd: {ty : Type} -> Show ty =>     (obj : ty) -> {ty : Type} -> Show ty => (obj : ty) -> String

不错,现在可以编写printf 了:

printf : (fmt : String) -> PrintfType(toFmt $ unpack fmt)printf fmt =printfAux (toFmt $ unpack fmt) [] where printfAux :(fmt : Fmt)-> ListChar ->PrintfType fmt printfAux (FArg fmt) acc = \obj => printfAux fmt (acc ++unpack (show obj)) printfAux (FChar c fmt) acc = printfAux fmt (acc ++[c]) printfAux FEnd acc = pack acc

可见,PrintfType(toFmt $ unpack fmt) 出现在了类型签名中,意味着 printf 的整个类型依赖于输入参数 fmt!但是 unpack fmt 是什么意思?因为 printf 接受 fmt:String,我们应当先将其转换成 List Char,因为要在 toFmt 中匹配该字符串;据我所知,Idris 不允许用同样的方法匹配原始的 String。类似地,在调用 printfAux 之前要进行 unpack fmt,因为它也接受 List Char 作为结果累加器。

我们来看一下 printfAux 的实现:

1、(FArg     fmt)。这里返回一个 lambda 函数,该函数接受 obj 并调用 show,然后使用 ++ 运算符将其添加到 acc中。

2、(FChar     c fmt)。将 c 添加到 acc,并再次使用 fmt 调用 printfAux。

3、FEnd。由于     acc 的类型为 List Char,但我们要返回     String (根据 PrintfType 的最后一种情况),因此对其调用 pack。

最后,测试一下printf:

printf.idr
main : IO ()main =putStrLn $ printf "Mr.John has * contacts in *." 42 "New York"

上述代码的输出为:Mr. John has 42 contacts in "New York".。但如果我们没有给printf 提供 42 会怎样?

Error: While processing right hand side ofmain. When unifying:   ?ty -> PrintfType (toFmt [assert_total (prim__strIndex "Mr. Johnhas * contacts in *." (prim__cast_IntegerInt (natToInteger (length"Mr. John has * contacts in *.")) - 1))])and:   StringMismatchbetween: ?ty -> PrintfType (toFmt[assert_total (prim__strIndex "Mr. John has * contacts in *."(prim__cast_IntegerInt (natToInteger (length "Mr. John has * contacts in*.")) - 1))]) and String.test:21:19--21:68 17|     printfAux (FChar c fmt) acc =printfAux fmt (acc ++ [c]) 18|     printfAux FEnd acc = pack acc 19 | 20 |main : IO () 21 |main = putStrLn $ printf "Mr. John has * contacts in *." "NewYork"                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^Warning: compiling hole Main.main

Idris 会检测出错误,然后产生一个类型不匹配错误!这就是使用类型优先的语言实现类型安全的 printf 的做法。如果你对此有兴趣,可以看看 Will Crichton 的实验(https://willcrichton.net/notes/type-safe-printf/),该实验大量应用了前面介绍的异构列表。

这种方法的缺点也应该很明显了:在 Rust 中,类型系统的语言和主语言不一样,但在 Idris 中,两者是相同的,这就是为什么能将类型级别的函数定义成一个返回 Type 的普通函数,并在类型签名中调用的原因。更进一步,因为 Idris 采用依赖类型,你甚至可以根据某些运行时参数来计算类型。

我猜到有人会问:用宏实现 printf 有什么问题?毕竟,Rust 中的 println! 也很好用。问题在于宏。自己想象:为什么编程语言需要大量的宏?因为我们需要扩展它们。为什么需要扩展?

因为编程语言无法满足要求:我们无法用正则语言抽象来宝石表示,这就是为什么要用一次性的元抽象来扩展语言。之前我谈过这种方法很糟糕,因为宏系统并不了解它所操作的语言;实际上,Rust 中的过程式宏也不过是 M4 预处理器,只不过名字好听一点而已。你们只不过是在语言中集成了 M4。

当然,这比外部的 M4 要好,但不管怎样,它也是上个世纪的方法;过程式宏甚至无法处理抽象语法书,因为用于编写过程式宏的一个常用结构 syn::Item 的本质是具体语法树(concrete syntax tree),或者叫“解析树”。相反,类型是宿主语言的重要组成部分,因此,如果我们能用类型来表达程序化的抽象,就会重用语言抽象,而不是依赖于一次性的机制。

理想情况下,一门编程语言不应该有宏,或只有轻量级的语法重写规则(像 Scheme的 extend-syntax 或 Idris 的语法扩展),来保证语言的一致性,并保证它能解决任务。

尽管如此,Idris还是通过引入 Type 类型(所有类型的类型)解决了第一个二元性:“值和泛型”。于是,它也解决了一系列其他的问题,如递归和类型层面的归纳问题、函数和 trait 机制问题,等等,而这反过来可以让我们尽可能用同一种语言编写程序,甚至能处理极端泛化的代码。例如,你甚至可以用 List Type 表示类型的列表,和 List Nat 或 List String 没什么两样。这一切都要归功于增量式的层次结构:简单来说,Type是类型 Type 1,Type 1 是类型 Type 2,以此类推。由于 Data.List 的通用名 a 隐含了类型 Type,因此它也可以是 Nat 或 String;在后者的情况下,a 会被推断为 Type 1。这种类型的无限序列可以防止 Russell 悖论。

但是,Idris 并不是一门简单的语言。上面仅有 20 行的 printf 示例已经用到了很多特性,如可归纳数据类型、依赖模式匹配、隐含、类型约束等。此外,Idris 还支持 computational effects、elaborator reflection、coinductive data types等许许多多用于理论证明的特性。有了这么多类型特性,人们通常会去研究语言本身的机制,而不是去做有意义的事情。我很难相信,在现在的情况下,依赖类型能在大规模应用中找到用武之地,因为目前在编程语言的世界中,它只不过是编程语言研究人员的玩具,也只有像我这样的爱好者才会关注。只有依赖类型还是太底层了。


Zig:更简单,但太系统化

 

在 Zig中,类型是一等公民。类型可以被赋值给变量,作为参数传递给函数,还能由函数返回。

——Zig手册

最后来谈一谈 Zig 编程语言。下面是 Zig 中编译时 printf 的实现:

printf.zigconst std = @import("std");fn printf(comptime fmt: []const u8, args: anytype)anyerror!void {    const stdout =std.io.getStdOut().writer();    comptime vararg_idx: usize = 0;    inline for(fmt) |c| {        if (c =='*') {            tryprintArg(stdout, args[arg_idx]);            arg_idx+= 1;        } else {            trystdout.print("{c}", .{c});        }    }    comptime {        if(args.len != arg_idx) {           @compileError("Unused arguments");        }    }}fn printArg(stdout: std.fs.File.Writer, arg: anytype)anyerror!void {    if(@typeInfo(@TypeOf(arg)) == .Pointer) {        trystdout.writeAll(arg);    } else {        trystdout.print("{any}", .{arg});    }}pub fn main() !void {    tryprintf("Mr. John has * contacts in *.\n", .{ 42, "New York"});}

这里,我们使用了一个名为 comptime 的特性。comptime 的函数参数意味着它必须在编译时确定。这不仅可以带来更激进的优化,还打开了“元编程”的大门,最值得一提的就是它没有宏级别或类型级别的子语言。上面的代码无需太多解释,这段逻辑应该非常好懂,不像 printf.idr 那样晦涩。

如果省略 42,Zig 就会报告编译错误:

An error occurred:/tmp/playground2454631537/play.zig:10:38: error: field index 1outside tuple 'struct:33:52' which has 1 fields tryprintArg(stdout, args[arg_idx]); ^/tmp/playground2454631537/play.zig:33:15: note: called from here try printf("Mr. Johnhas * contacts in *.\n", .{ "New York" }); ^/tmp/playground2454631537/play.zig:32:21: note: called from herepub fn main() !void { ^

在开发 printf 的过程中,我感受到的唯一不便之处就是大量的错误,就像 C++ 模板一样。但是,我承认这个问题可以通过更明确的类型约束解决(至少有办法绕过)。

总体而言,Zig 的类型子系统似乎非常合理:所有类型的类型叫 type,使用 comptime,可以在编译时通过正常的变量、循环、过程等计算类型。我们甚至可以通过 @typeInfo、@typeName 和 @TypeOf 内置函数进行类型反射!没错,我们不需要再依赖运行时的值,但如果不需要理论证明,那么完整功能的依赖类型可能有点杀鸡牛刀了。

Zig什么都好,可它只是一个系统语言。其官网对 Zig 的描述为“通用编程语言”,但我很难同意这一点。没错,你可以用 Zig 编写任何软件,但应该这样做吗?根据我维护 Rust 和 C99 的高层代码来看,答案是否定的。第一个原因是安全性:如果需要让一种系统语言安全,就要让程序员处理借出检查器和所有权问题(或类似的问题),而这些与业务逻辑毫无关系(这非常麻烦);否则,如果你选择 C 式的手工内存管理,程序员就要花费大量时间调试程序,并且寄希望于-fsantinize=address 能显示有用的信息。更有甚者,如果你要在指针上建立新的抽象,就会引入&str、AsRef<str>、Borrow<str>、Box<str> 等等。问题是我只想要一个 UTF-8 字符串而已;绝大部分情况下我并不在乎是哪一种。

第二个原因是语言的运行时:对于系统语言而言,为了避免性能降低,其运行时要尽可能小——不带默认的 GC,没有默认的事件循环,等等。但对于特定应用来说,运行时是有必要的,比如有时需要异步运行时。所以,你不得不用某种方式来处理自定义运行时的代码。

这里就会遇到一系列新问题:例如,语言中有 async,但没有任何工具来抽象同步和异步函数,就意味着你必须将语言分成两部分:同步和异步。假设你有一个泛型的高阶函数库,就只能标记为 async,才能接受所有用户提供的回调。

为了解决这个问题,你不得不实现某种形式的多态,而这仍在研究中。高级语言需要处理的问题更少,这也是为什么绝大部分软件都是用 Java、C#、Python 和 JavaScript 编写的。在 Golang 中,概念上任何函数都是 async,本身就提高了一致性,而不需要复杂的类型特性。相反,Rust 本身就已经很复杂,但仍没有任何标准方式来编写真正的泛型异步代码。

Zig 仍然可以在 Web 浏览器、解释器、操作系统内核等大型项目中派上用场,因为没人希望这些软件会无故崩溃。Zig 的底层编程特性可以带来方便的内存操作和硬件操作,而它在元编程方面的特性能带来更容易理解的代码结构。而将 Zig 带入高级语言代码,只会增加精神负担,并没有实际的好处。


结束语

 

静态语言会强制进行编译时检查,这很好。但这会带来了二元性和不一致,这是缺点。而动态语言受这些影响相对较少,但它们缺乏编译时检查。理想的解决方案应该吸取两家之长。

我们应该重新思考编程语言。

参考文献

  • Edsger Dijkstra. n.d. “On the Teaching of Programming, i.e. On theTeaching of Thinking.”https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/EWD473.html.

  • Edwin Brady. n.d. “Type-Driven Development with Idris.” ManningPublications Co.https://www.manning.com/books/type-driven-development-with-idris.

  • Zig developers. n.d. “Introducing the Compile-Time Concept.”https://ziglang.org/documentation/0.9.0/#Introducing-the-Compile-Time-Concept.


评论


评论1:

炫酷的类型系统并不一定都实用。Go 的类型系统非常小,就已经能满足 Google 内部的许多服务器端需求了。

许多 bug 的原因都是违反了不可变原则。在某个地方做了某种假设,而在另一个地方却破坏了这种假设,这就是违反不可变原则。

类型系统能避免一部分违反不可变原则的发生。因此,人们尝试扩展型系统,来防止更多的违反不可变原则的情况。但这就带来了另一层灰色的抽象。一些不可变原则并不能很好地表示成类型,强行表示就非常别扭。而我们真正需要的是用全局分析代替人工检查。

Rust 的借出检查器就是一种不可变原则检查器。它会明确地进行自动全局分析,并报告违反不可变原则的情况。这是编程语言设计上真正的进步,也是Rust 的主要贡献。

这才是正确的方向。全局分析还能解决其他问题,比如死锁检测等。如果在同一条路径上,P 在 Q 之前枷锁,那么在所有路径上 P 都必须在 Q 之前加锁。不能有任何路径导致 P 被加锁两次。Rust 在引用计数上有一个类似的问题,只能在运行时检查,其原理和锁差不多。

评论2:

类型系统非常实用,尤其在重构的时候。

但是,就算没有类型检查器,选择良好的命名规则也很不错。

我希望鼓吹类型系统的人不要闭门造车,应该花点时间接触一下动态语言,才能得出更客观的结论。

参考链接:

https://hirrolot.github.io/posts/why-static-languages-suffer-from-complexity#


新程序员003》正式上市,50余位技术专家共同创作,云原生和数字化的开发者们的一本技术精选图书。内容既有发展趋势及方法论结构,华为、阿里、字节跳动、网易、快手、微软、亚马逊、英特尔、西门子、施耐德等30多家知名公司云原生和数字化一手实战经验!

   
   
     
☞被骂惨的 Windows 11 还是“真香”了:下月将支持 Android 应用,产品满意度历代最高!
每天敲代码不到 1 小时?这就是程序员的“真实”日常!
cURL作者狂怼某500强公司,开源维护者是否应当“白打工”?
登录查看更多
0

相关内容

【2021新书】面向对象的Python编程,418页pdf
专知会员服务
70+阅读 · 2021年12月15日
专知会员服务
79+阅读 · 2021年7月3日
【干货书】Python参考手册,210页pdf
专知会员服务
63+阅读 · 2021年4月30日
专知会员服务
57+阅读 · 2021年4月7日
专知会员服务
91+阅读 · 2020年12月26日
专知会员服务
81+阅读 · 2020年9月28日
【2020新书】C++20快速语法参考,第4版,209页pdf
专知会员服务
71+阅读 · 2020年8月5日
【2020新书】高级Python编程,620页pdf
专知会员服务
235+阅读 · 2020年7月31日
Go中的泛型:激动人心的突破
AI前线
0+阅读 · 2022年4月7日
“C 不再是一种编程语言!”
CSDN
0+阅读 · 2022年4月4日
那些有用但不为大家所熟知的 Java 特性
AI前线
0+阅读 · 2022年2月16日
K8s 为什么这么复杂?
CSDN
0+阅读 · 2022年2月10日
那些有用但不为大家所熟知的Java特性
AI前线
0+阅读 · 2022年2月8日
用70行Python编写一个概率编程语言
CSDN
0+阅读 · 2022年2月2日
在Python中使用SpaCy进行文本分类
专知
24+阅读 · 2018年5月8日
国家自然科学基金
5+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
2+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
2+阅读 · 2009年12月31日
Arxiv
0+阅读 · 2022年4月19日
Arxiv
0+阅读 · 2022年4月18日
Arxiv
26+阅读 · 2018年8月19日
VIP会员
相关VIP内容
【2021新书】面向对象的Python编程,418页pdf
专知会员服务
70+阅读 · 2021年12月15日
专知会员服务
79+阅读 · 2021年7月3日
【干货书】Python参考手册,210页pdf
专知会员服务
63+阅读 · 2021年4月30日
专知会员服务
57+阅读 · 2021年4月7日
专知会员服务
91+阅读 · 2020年12月26日
专知会员服务
81+阅读 · 2020年9月28日
【2020新书】C++20快速语法参考,第4版,209页pdf
专知会员服务
71+阅读 · 2020年8月5日
【2020新书】高级Python编程,620页pdf
专知会员服务
235+阅读 · 2020年7月31日
相关资讯
Go中的泛型:激动人心的突破
AI前线
0+阅读 · 2022年4月7日
“C 不再是一种编程语言!”
CSDN
0+阅读 · 2022年4月4日
那些有用但不为大家所熟知的 Java 特性
AI前线
0+阅读 · 2022年2月16日
K8s 为什么这么复杂?
CSDN
0+阅读 · 2022年2月10日
那些有用但不为大家所熟知的Java特性
AI前线
0+阅读 · 2022年2月8日
用70行Python编写一个概率编程语言
CSDN
0+阅读 · 2022年2月2日
在Python中使用SpaCy进行文本分类
专知
24+阅读 · 2018年5月8日
相关基金
国家自然科学基金
5+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
2+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
2+阅读 · 2009年12月31日
Top
微信扫码咨询专知VIP会员