重构 Raku 的 Junction
— 焉知非鱼Reconstructing Raku’s Junctions
重构 Raku 的 Junction #
Raku 中的 junction 很酷,但乍一看它们并没有遵循静态类型化的规则。我对它们的形式化类型语义很好奇,所以我从功能、静态类型的角度对 junction 进行了解构和重构。
Raku 中的 Junction #
Raku 有一个整洁的功能叫做 Junction。Junction 是一个无序的复合值。当使用 junction 代替值时,会对每个结点(junction)元素进行操作,结果是所有这些操作符的返回值的结点(junction)。当在布尔上下文中使用 junction 时,结点(junction)会折叠成一个值。Junction 的类型可以是 all(&
)、any(|
)、one(^
) 或 none
(空结点)。
例如:
my $j = 11|22; # short for any(11,22)
if 33 == $j + 11 {
say 'yes';
}
say so 3 == (1..30).one; #=> True
say so ("a" ^ "b" ^ "c") eq "a"; #= True
函数 so
强制使用布尔上下文。
Junction 有 Junction
类型,我很好奇 Junction 的类型规则,因为乍一看有些奇怪。比方说我们有一个函数 sq
从 Int
到 Int
。
sub sq(Int $x --> Int) { $x*$x }
my Int $res = sq(11); # OK
say $res; #=> 121
现在让我们定义一个类型为任何 Int
值的 Junction。
my Junction $j = 11 | 22;
当我们将 sq
应用于 $j
时,我们没有得到一个类型错误,即使函数的类型是 :(Int --> Int)
,Junction 的类型是 Junction
。相反,我们得到的是一个结果的 Junction。
say sq($j); #=> any(121, 484)
如果我们像之前一样将其赋值给一个类型为 Int
的变量,我们会得到一个类型错误。
my Int $rj = sq($j); #=> Type check failed in assignment to $rj; expected Int but got Junction (any(121, 484))
取而代之的是,现在返回值的类型为 Junction
。
my Junction $rj = sq(11|22); # OK
所以,Junction 类型可以代替任何其他类型,但这样一来,操作也变成了 Junction。
另一方面,Junction 是由其组成值隐式类型的,尽管它们看起来是不透明的 Junction
类型。例如,如果我们创建了一个由 Str
值组成的 Junction,并试图将这个 Junction 的值传递到 sq
中,我们会得到一个类型错误。
my $sj = '11' | '22';
say $sj.WHAT; #=>(Junction)
my Junction $svj = sq($sj); #= Type check failed in binding to parameter 'x'; expected Int but got Str ("11")
Junction 不遵循静态类型规则 #
虽然这样做是有道理的(如果原始函数期望使用 Int
,我们不希望它与 Str
一起工作),但这确实违背了静态类型化的规则,即使是子类型化。如果一个参数的类型是 Int
,那么可以使用类型图中低于它的任何类型来代替。但是 Int
和 Junction
的简化类型图如下。
Int -> Cool -> Any -> Mu <- Junction
所以 Junction 永远不是 Any
以下任何东西的子类型。因此,将 Junction 放在类型为 Any
或其子类型的槽中应该是一个类型错误。
此外,由于 Junction 类型是不透明的(即它不是一个参数化的类型),它不应该持有任何关于 Junction 内部值的类型的信息。然而它却对这些不可见、不可访问的值进行了类型检查。
那么这里到底发生了什么?
一个工作假设 #
一个工作假设是,Junction 类型并不真正取代任何其他类型:它只是一个语法糖,使它看起来如此。
重构 Junction 的第一部分:类型 #
让我们试着重建这个。我们的目的是想出一个数据类型和一些动作,以复制观察到的 Raku Junction 的行为。首先我们讨论一下类型,为了清晰起见,使用 Haskell 符号。然后我介绍 Raku 中的实现。这个实现将像 Raku 的原生 Junction 一样,但没有神奇的语法糖。通过这种方式,我证明了 Raku 的 Junction 毕竟遵循了正确的类型规则。
Junction 类型 #
Junction 是一个由 Junction 类型 JType
和一组值组成的数据结构。为了方便起见,我将这个值集限制为单一类型,同时也是因为混合类型的 Junction 其实没有什么意义。我使用一个列表来模拟这个集合,同样是为了方便。因为 Junction 可以包含任何类型的值,所以它是一个多态的代数数据类型。
data JType = JAny | JAll | JOne | JNone
data Junction a = Junction JType [a]
应用结点 #
对一个 Junction 做任何事情都意味着对它应用一个函数。我们可以考虑三种情况,我为每一种情况介绍一个特别定制的操作符。
- 将非 Junction 函数应用于 Junction 表达式
(•○) :: (a -> b) -> Junction a -> Junction b
- 将 Junction 函数应用于非 Junction 表达式。
(○•) :: Junction (b -> c) -> b -> Junction c
- 将 Junction 函数应用于 Junction 表达式,创建一个嵌套 Junction。
(○○) :: Junction (b -> c) -> Junction b -> Junction (Junction c)
为了方便,我们还可以在 Junction a 和 a 之间创建自定义比较运算符。
-- and similar for /-, >, <, <=,>=
(○==•) :: Junction a -> a -> Bool
折叠 Junction #
那么我们就有了 so
,布尔强制函数。它的作用是将一个布尔的 Junction 折叠成一个布尔。
so :: Junction Bool -> Bool
最后我们有 collapse
,它从一个 Junction 返回值,前提是它是一个 Junction,所有存储的值都是一样的。
collapse :: (Show a,Eq a) => Junction a -> a
这似乎是一个奇怪的函数,但由于 Junction 的行为,它是必要的。正如我们将看到的,上述语义意味着 Junction 是贪婪的:如果一个函数的一个参数是 Junction,那么所有其他参数也会成为 Junction,但 Junction 中的所有值都是相同的。我已经在"贪婪 Junction 的奇怪情况“中讨论过这个问题,但我们现在可以将这种行为形式化。
重新审视贪婪 Junction 的奇怪情况 #
假设我们有一个两个参数的函数 f :: a -> b -> c
,我们对第一个参数应用一个结点 j :: Junction
a 应用到第一个参数 f •○ j
上,那么结果是一个部分应用的函数,包裹在一个 Junction 上:fp :: Junction b -> c
。如果我们现在想用 fp ○• v
将这个函数应用于一个非结点的值 v :: b
,那么结果就是 Junction c
类型的。
现在,让我们考虑类型 c
是 forall d . (a -> b -> d) -> d
的特殊情况。所以我们有 Junction
(forall d . (a->b->d) -> d
)。这是一个函数,它接受一个函数参数并返回该函数的返回类型的东西。我们使用 forall
,所以 d
可以是任何东西,但在实践中我们希望它是 a
或 b
。
假设我们将这个函数(称它为 p
)应用于 fst :: a->b->a
,使用 p ○• fst
,那么我们得到 Junction a
。但是如果我们将它应用于 snd :: a->b->b
,使用 p ○• snd
,那么我们得到 Junction b
。
这就是形式上基于类型的分析,为什么我们不能从一个 pair 中返回一个非 Junction 的值,在”贪婪 Junction 的奇怪情况“中已经解释过。而这也是我们需要 collapse
函数的原因。
重构 Junction 的第2部分:Raku 的实现。 #
我们从创建 Junction 类型开始,为四种 Junction 类型使用一个枚举,为实际的 Junction 数据类型使用一个角色。
# The types of Junctions
enum JType <JAny JAll JOne JNone >;
# The actual Junction type
role Junction[\jt, @vs] {
has JType $.junction-type=jt;
has @.values=@vs;
}
接下来是四种类型的 Junction 的构造函数(下划线,避免与内建函数的名称冲突)。
our sub all_(@vs) {
Junction[ JAll, @vs].new;
}
our sub any_(@vs) {
Junction[ JAny, @vs].new;
}
our sub one_(@vs) {
Junction[ JOne, @vs].new;
}
our sub none_(@vs) {
Junction[ JNone, @vs].new;
}
将一个(单参数)函数应用于 junction 参数。
sub infix:<●○>( &f, \j ) is export {
my \jt=j.junction-type;
my @vs = j.values;
Junction[ jt, map( {&f($_)}, @vs)].new;
}
要将 Junction 内的函数应用于非 Junction 的参数:
sub infix:<○●>( \jf, \v ) is export {
my \jt=jf.junction-type;
my @fs = jf.values;
Junction[ jt, map( {$_( v)}, @fs)].new;
}
将一个函数应用于两个 junction 参数,相当于将一个 junction 内的函数应用于一个 junction。这里有一个复杂的问题。Raku 对嵌套施加了一个排序,即所有的嵌套总是外嵌套。因此,我们必须检查 junction 的类型,如果需要的话,我们必须交换映射。
sub infix:<○○>( \jf, \jv ) is export {
my \jft= jf.junction-type;
my @fs = jf.values;
my \jvt = jv.junction-type;
my @vs = jv.values;
if (jvt == JAll and jft != JAll) {
Junction[ jvt, map( sub (\v){jf ○● v}, @vs)].new;
} else {
Junction[ jft, map( sub (&f){ &f ●○ jv}, @fs)].new;
}
}
为了完整,这里是 ○==●
的定义。○!=●
、○>●
等的定义是类似的。
sub infix:< ○==● >( \j, \v ) is export {
sub (\x){x==v} ●○ j
}
接下来我们有 so
,它把布尔值的 junction 变成了布尔值。
our sub so (\jv) {
my @vs = jv.values;
given jv.junction-type {
when JAny { elems(grep {$_}, @vs) >0}
when JAll { elems(grep {!$_}, @vs)==0}
when JOne { elems(grep {$_}, @vs)==1}
when JOne { elems(grep {$_}, @vs)==0}
}
}
最后我们有 collapse
,正如贪婪 Junction 的文章中所定义的那样, collapse
返回 Junction 的值,只要它们都是一样的。
our sub collapse( \j ) {
my \jt=j.junction-type;
my @vvs = j.values;
my $v = shift @vvs;
my @ts = grep {!($_ ~~ $v)}, @vvs;
if (@ts.elems==0) {
$v
} else {
die "Can't collapse this Junction: elements are not identical: {$v,@vvs}";
}
}
Junction 清理 #
现在我们再来看看我们的工作假说,将 Raku 的 Junction 上的动作解释为上述类型和操作符的语法糖。
sub sq(Int $x --> Int) { $x*$x }
my Junction $j = 11 | 22;
my Junction $rj = sq($j);
去语法塘后这变成了:
my Junction $j = any_ [11,22];
my Junction $rj = &sq ●○ $j;
类似地,
if ($j == 42) {...}
变成了:
if (so ($j ○==● 42)) {...}
和其他布尔上下文类似。
如果我们仔细看贪婪 Junction 文章中的 pair 例子,那么将 junction 应用到一个有多个参数的函数上:
my Junction \p1j = pair R,(42^43);
去语法塘后变为:
my Junction \p1j = &pair.assuming(R) ●○ one_ [42,43];
我们使用 .assuming()
是因为我们需要部分应用。不管我们是先应用非 Junction 参数还是 Junction 参数,都没有关系。
my \p1jr = ( sub ($y){ &pair.assuming(*,$y) } ●○ one_ [42,43] ) ○● R;
最后,举一个两个参数都是 Junction 的例子。由于 ○○
的定义,应用的顺序并不重要。
sub m(\x,\y){x*y}
my \p4 = ( sub (\x){ &m.assuming(x) } ●○ any_ [11,22] ) ○○ all_ [33,44];
my \p4r = ( sub (\x){ &m.assuming(*,x) } ●○ all_ [33,44] ) ○○ any_ [11,22];
结论 #
从 Raku 的 junction 的神奇类型行为实际上是语法糖的假设出发,我使用多态代数数据类型重构了 junction 类型和它的动作,并表明 Raku 的行为作为语法糖的解释对于所提出的实现是成立的。换句话说,Raku 的 Junction 确实遵循静态类型规则。
原文链接: https://gist.github.com/wimvanderbauwhede/19cc1e8d04e9a477f58cfe7288a6172e