子类型规则

子类型规则指定Felix何时可以执行隐式强制。

记录

记录同时支持宽度和协变深度子类型。

宽度子类型

接受特定字段集的参数可以通过附加字段传递一个记录值。Felix插入一个强制,该强制只使用必需的字段构建一个新记录:

fun f(p : (a:int, b: int)) => p.a + p.b;
f (a=1,b=2,c=3); // OK, c field is discarded

深度子类型

如果B是P的子类型,则接受P类型字段的记录的参数将接受B类型字段的记录:

fun f(p : (a=int, b=(c:int, d:int))) => p.a + p.b.c + p.b.d;
f (a=1,b=(c=2,c=3,d=4)); // OK, b value is coerced

在本例中,字段的类型 b 参数的强制为字段类型 b 当宽度子类型发生变化时。

深度和宽度子类型可以同时使用并递归应用。

元组和数组子类型

元组和数组支持协变深度子类型。例如:

f(p: (a:int,b:int), d:int) => p.a + p.b +p.c;
println$ f ((a=1,b=2,c=3,42); // OK, coerce first component

尽管子类型化不支持子类型化,但子类型化并不支持这种特殊的数组大小写。这是因为在超载的情况下很可能会令人困惑。

多态变异体亚型

多态变体支持宽度子类型和协变深度子类型,但是宽度子类型规则与记录相反,参数必须具有较少的字段:

typedef psub = (`A | `B | `C);
typedef psup = (`A | `B | `C | `D);
var v = `A :>> psub;
fun f(p: psup) => match p with
  | `A => "A"
  | `B => "B"
  | `C => "C"
  | `RD=> "D"
  endmatch
;
println$ f v;

函数 f 可以处理4种情况,因此传递只能是其中三种情况之一的参数是安全的。

匿名和类型子类型

相似元组匿名和支持协变深度子类型,但不支持宽度子类型,原因相同。如果一个带有bool参数的函数接受一个单位参数,即使在原则上1是2的子类型,也会令人困惑。

功能子类型

函数支持子类型化,域是逆变的,密码域是协变的。

抽象指针子类型

抽象指针的定义如下:

typedef fun rptr (T:TYPE) : TYPE =>  (get: 1 -> T);
typedef fun wptr (T:TYPE) : TYPE =>  (set : T -> 0);
typedef fun rwptr (T:TYPE) : TYPE => (get: 1 -> T, set : T -> 0);

因此,由于记录类型遵循记录的子类型规则。尤其是读写指针类型 rwptr 是两个只读指针的子类型 rptr 只写指针 wptr 按子类型规则的记录。

rptr 是通过记录的深度子类型规则和函数密码域的协方差的组合而协变的。

wptr 通过记录的深度子类型化规则和函数域的逆变规则的组合实现逆变。

rwptr 是不变的,因为它必须同时协变和逆变。

机器指针子类型

Felix有三种主要的机器指针类型,一种是只读指针,一种是只写指针,另一种是另两种类型的子类型。指向的类型是不变的。

虽然在原则上,机器指针应该遵循抽象指针的模型,但是深度子类型化不受支持,因为它一般不能具体实现。

但是有一个特殊的例外。原则上,如果强制是幻象,也就是说,它影响类型系统,但不更改底层计算机地址,则可以实现方差。Felix认为只写机器指针指向 uniq T 作为指向的只写指针的子类型 T . 这是必要的,以便程序:

proc storeat[T] ( p: &>T, v: T) = { _storeat (p,v); }

使用指向 uniq T . 如果没有这个规则,就不可能对唯一类型变量赋值,这种赋值实际上是模型移动。

唯一子类型

类型 uniq T 是一个亚型 T . 这意味着T类型的参数可以传递类型为的参数 uniq T ,放弃唯一性。这是因为编译器后端无论如何都会丢弃唯一性构造函数,因此在验证唯一类型规则之后,绑定退化为非唯一操作。

用名义类型分型

Felix通过允许用户定义强制,允许单态命名类型形成子类型关系。

有符号整数

例如,Felix提供:

supertype vlong: long = "(long long)$1";
supertype long: int = "(long)$1";
supertype int : short= "(int)$1";
supertype short : tiny = "(short)$1";

例如,这种亚型胁迫是可传递的, int 是一个亚型 long . Felix会自动产生一个复合强制。如果有一种以上的成分,复合材料必须有同样的效果,因为Felix会任意选择一种。

考虑以下功能:

fun add(x:int, y:int):int => x + y;
fun add(x:long, y:long):int => x + y;
fun add(x:vlong, y:vlong):int => x + y;

与上面的子类型规则一起,函数的行为方式与C中的加法相同;也就是说,就像应用了C积分提升规则一样。

正符号整数

Felix为普通的C有符号整数类型和精确的C有符号整数类型提供了子类型。

supertype int64: int32 = "(int64_t)$1";
supertype int32 : int16 = "(nt32_t)$1";
supertype int16 : int8  "(int16_t)$1";

但是,有符号类型和无符号类型之间、普通类型和精确类型之间或无符号类型之间没有转换。

真实到复杂

浮点实数之间没有转换。C定义了从float到double和double到long double的提升,但实际上这些都是错误的:数值分析表明,安全的转换实际上是朝着另一个方向进行的。

但是浮点实数可以嵌入相同精度的复数中:

supertype fcomplex: float = "::std::complex<float>($1,0.0f)";
supertype dcomplex: double = "::std::complex<double>($1)";
supertype lcomplex: ldouble = "::std::complex<long double>($1)";

注意,这意味着任何复杂参数都将接受浮点实数参数。

烦恼

很烦人的是我们不能隐式地将整数嵌入浮点。但是,要想让它起作用,必须 double 独自一人。要将嵌入到所有浮动类型中,需要对浮动类型进行子类型化以避免歧义。