rakulang

重构 Raku 的 Junction

Sun Oct 4, 2020

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