rakulang, dartlang, nimlang, golang, rustlang, lang lang no see

重构 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 的类型规则,因为乍一看有些奇怪。比方说我们有一个函数 sqIntInt

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,那么可以使用类型图中低于它的任何类型来代替。但是 IntJunction 的简化类型图如下。

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 类型的。

现在,让我们考虑类型 cforall d . (a -> b -> d) -> d 的特殊情况。所以我们有 Junction(forall d . (a->b->d) -> d)。这是一个函数,它接受一个函数参数并返回该函数的返回类型的东西。我们使用 forall,所以 d 可以是任何东西,但在实践中我们希望它是 ab

假设我们将这个函数(称它为 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