APartSML(5)——结构体和签名

Posted Jan 22, 2025

By ZoeyWang

22 min read

APartSML(5)——结构体和签名

1.what is type inference

静态类型语言statically typed languages：在编译时（程序运行前），每个binding的类型都已经确定，因此类型错误会在编译时提醒，比如Java，C，ML
动态类型语言dynamically typed languages：每个binding的类型不会提前确定，在运行时才会确定，因此类型错误会在运行时报错，比如Racket，Ruby，Python

不同于Java和C，ML是隐式类型，即不需要程序员写下明确的bindings类型，ML中的type-checker会同时进行类型推断和类型检查。ML中的类型推断和参数多态polymorphism也往往关联，但是这实际上是两个概念，比如Java支持多态但是不支持推断。

ML中的类型推断算法如下：

按顺序决定bindings的类型，使用更早的bindings类型来推导后面bindings的类型
对每个val或者fun binding，都会分析关于其类型的事实，比如表达式x+1，那么说明x一定是int类型，类似的事实还有各种函数调用，样式匹配等
对于无约束的类型，使用类型变量type variables，即类型为多态
只有变量和值有多态类型

基于上述过程，ML中可以不使用显式类型，除非使用了#1这种特征，那么就无法推断出具体的类型而报错，一个简单的类型推断例子

  
val x = 42
fun f(y,z,w) = if y then z+x else 0

x的类型一定是int
由于y在判断条件里，y的类型是bool
由于表达式z+x而x是int，z的类型也是int
w没有被使用，可以是任何类型
函数f的两个分支都返回int

因此f的类型为bool * int * 'a ->int.

ML类型推断可以推出多态类型，比如下面函数中，xs只能推出是list，但是不能确定是什么类型的list，int list 和string list都可以通过该函数计算列表长度

  
fun length xs =
    case xs of
        [] => 0
      | x::xs' => 1 + (length xs')

'a list -> int

2.mutual recursion

ML规则里每个bindings只能使用更早之前的bindings，如果需要函数f调用函数g，函数g再调用f怎么实现（相互递归调用mutual recusion），ML里提供了关键词and。

定义一个函数，输入一个整数列表，判断状态值是不是1212这样的序列，必须以2为结束，定义两个局部函数s_need_one和s_need_two，第二个函数前面不是fun，而是and，表示这两个函数会一起进行type-checker，允许不按照顺序彼此调用。计算科学中的许多问题都可以建模成这种有限状态机（fi nite state machines）和相互递归函数

  
fun match xs =
    let fun s_need_one xs =
            case xs of
                [] => true
              | 1::xs' => s_need_two xs'
              | _ => false
        and s_need_two xs =
            case xs of
                [] => false
              | 2::xs' => s_need_one xs'
              | _ => false
    in
        s_need_one xs
    end;

- use "mutual.sml";
[opening mutual.sml]
val match = fn : int list -> bool
val it = () : unit
- match [1,2,1,2,1,2];
val it = true : bool

datatype bindings也可以相互递归调用，下面代码中定义类型t1和t2相互指向对方

  
datatype t1 = Foo of int
            | Bar of t2
and t2 = Baz of string
        |Quux of t1;

fun no_zero_or_empty_strings_t1 x =
    case x of
        Foo i => i <> 0
      | Bar y => no_zero_or_empty_strings_t2 y
and no_zero_or_empty_strings_t2 x =
    case x of
        Baz s => size s > 0
      | Quux y => no_zero_or_empty_strings_t1 y;

- use "mutual.sml";
[opening mutual.sml]
datatype t1 = Bar of t2 | Foo of int
datatype t2 = Baz of string | Quux of t1
val no_zero_or_empty_strings_t1 = fn : t1 -> bool
val no_zero_or_empty_strings_t2 = fn : t2 -> bool

假设不想通过这种and的方式把两个函数必须写在一起，也可以通过高阶函数实现，即后面出现的函数作为参数传入到前面的函数中

  
fun no_zero_or_empty_strings_t1 (f,x) =
    case x of
        Foo i => i <> 0
      | Bar y => f y;
fun no_zero_or_empty_strings_t2 x =
     case x of
        Baz s => size s > 0
      | Quux y => no_zero_or_empty_strings_t1(no_zero_or_empty_strings_t2,y);

- use "mutual.sml";
val no_zero_or_empty_strings_t1 = fn : (t2 -> bool) * t1 -> bool
val no_zero_or_empty_strings_t2 = fn : t2 -> bool

3.modules for namespace management

ML支持把不同的bindings分到不同的命名空间（namespace），使用structures来定义modules，一个module包含了一系列bindings，包含值，函数，异常，数据类型和类型别名。

以下代码定义了一个模块MyMathLib，包括函数fact，half_pi和doubler，如果要调用模块里的函数，可以通过类似MyMathLib.fact获取

  
structure Name = struct bindings end

  
structure MyMathLib =
struct
fun fact x =
    if x = 0
    then 1
    else x * fact(x-1)

val half_pi = Math.pi / 2.0
fun doubler y = y + y
end;

- use "module.sml";
[opening module.sml]
structure MyMathLib : sig
  val fact : int -> int
  val half_pi : real
  val doubler : int -> int
end
- MyMathLib.fact 2;
val it = 2 : int

模块不是表达式，不能在函数内定义他们，或者存储在tuple，或者作为参数传递

4.Signatures

通过structure可以定义模块，通过signature可以定义模块的类型，提供了模块外调用模块函数必须严格遵循的接口（interface），signature包含数据类型，异常和类型bindings

  
signature MATHLIB =
sig
    val fact : int -> int
    val half_pi: real
    val doubler: int -> int
end;

structure MyMathLib :> MATHLIB =
struct
fun fact x =
    if x = 0
    then 1
    else x * fact(x-1)

val half_pi = Math.pi / 2.0

fun doubler y = y + y
end;

由于：>MATHLIB，结构MyMathLib必须要提供在MATHLIB中定义的内容，这些实现的类型必须符合签名中要求的类型，才能通过编译和类型检查。如果某个函数或数据类型的类型不匹配，或者没有提供签名中声明的内容，类型检查会失败。

5.hiding things

把函数的接口和实现分开，是实现可复用，具有鲁棒性编程的重要策略。比如在函数内部定义局部函数，这样后续修改这个实现也不会担心影响到其他函数。一些语言里会使用private字段来限制函数的可访问性。ML语言里使用signature来实现：任何没有在一个signature里被明确定义的不能被外部使用。

举一个模块的例子，该模块包含一个数据类型rational，一个异常，以及5个函数：（1）gcd：输入两个正整数，返回最大公约数（2）reduce：对有理数化简（3）make_frac：创建有理数（4）add：两个有理数相加（5）toString：把有理说编程字符输出

  
signature RATIONAL_A =
sig
    datatype rational = Whole of int
               |Frac of int * int
    exception BadFrac
    val make_frac : int * int -> rational
    val add : rational * rational -> rational
    val toString : rational -> string
end;


structure Rational1 :> RATIONAL_A =
struct

datatype rational = Whole of int
                   |Frac of int * int
exception BadFrac

(* x and y must > 0 *)          
fun gcd (x,y) =
    if x=y
    then x
    else if x < y
    then gcd(x,y-x)
    else gcd(y,x)

fun reduce r =
    case r of
        Whole _ => r
      | Frac(x,y) => if x=0
                     then Whole 0
                     else let val d = gcd(abs x, y)
                          in
                              if d=y
                              then Whole(x div d)
                              else Frac(x div d, y div d)
                          end

(* denominators > 0 no zero and no negative*)                  
fun make_frac (x,y) =
    if y = 0
    then raise BadFrac
    else if y < 0
    then reduce(Frac(~x, ~y))
    else reduce(Frac(x,y))

fun add (r1,r2) =
    case (r1,r2) of
        (Whole(i),Whole(j)) => Whole(i+j)
      | (Whole(i),Frac(j,k)) => Frac(j+k*i,k)
      | (Frac(j,k),Whole(i)) => Frac(j+k*i,k)
      | (Frac(a,b),Frac(c,d)) => reduce(Frac(a*d+b*c,b*d))

fun toString r =
    case r of
        Whole i => Int.toString i
      | Frac(a,b) => (Int.toString a) ^ "/" ^ (Int.toString b)
end;

对于模块，需要关注两类特征：

property：面向用户的特征，外部可见
invariants：内部实现的特征，仅模块内部可见

在上面实现的模块中，面向用户使用的特征有如下：

toString返回的是化简后的有理数字符串
没有代码会进行无限循环
没有代码会除以0
不存在分母为0的分数

模块内部的invariants有如下：

所有的分母一定大于0，如果用户输入分母小于0也会变成分子小于0
所有的有理数都是最简形式，不会出现分母为1的分数或者类似6/9

模块内部的invariants能够有效保证外部的property，但是当前模块仍然存在一个问题，我们希望用户通过调用Rational1.make_frac()来创建有理数，但是数据类型也是外部可见的，因为存在可能，用户直接创建Rational.Frac(1,0)，Rational.Frac(3,~2)，Rational.Frac(9,6)。为了解决这个方法，最直接的方法是在signature中去掉对rational的类型定义，但是这样也会出错，因为后面的函数类型定义使用到了rational数据类型，那么怎么可以在signature定义这个数据类型但是不被用户知道具体是什么，只需要知道存在即可，在signature中使用抽象类型abstract type，这样就没有其他方式去创建frac，只能通过make_frac()

  
signature RATIONAL_B =
sig
    type rational
    exception BadFrac
    val make_frac : int * int -> rational
    val add : rational * rational -> rational
    val toString : rational -> string
end;

6.A Cute Twist: Expose the Whole function

在上一小节中，要求类型Frac对外部不可见，Whole类型实际上是可见的，可以直接通过Rational1.Whole(2)这样来创建整数，为了不修改模块里的代码，可以在signature中把Whole当成函数定义，val Whole: int -> rational告知用户有一个函数Whole可以输入一个整数创建一个有理数，但是不知道具体实现内容，这样做到部分数据类型外部可见。

  
signature RATIONAL_C =
sig
    type rational
    exception BadFrac
    val Whole: int -> rational
    val make_frac : int * int -> rational
    val add : rational * rational -> rational
    val toString : rational -> string
end;

8.rules of signature matching

一个structure要和给定的signature匹配，才会进行type-check，具体有如下规则，此处的匹配和样式匹配不是一个概念

对于signature中的每个val-binding，structure都要有那个类型或者更通用类型的binding，比如structure的实现可能是多态的，但是signature中的定义不是
对于signature中的每个非抽象类型binding，structure要有相同的类型binding
对于signature中的每个抽象类型binding，structure要有能创建这个类型的相同binding（数据类型binding或者类型别名）

模块内的具体实现对用户而言是不可见的，因此可以用等价实现（equivalent implementation）来替换原先的实现，这也是软件开发中非常重要的任务，可以在不影响用户使用的前提下改进或者改变一个模块的内部实现过程

  
structure Rational2 :> RATIONAL_A =
struct
datatype rational = Whole of int
                   |Frac of int * int
exception BadFrac

fun make_frac (x,y) =
    if y = 0
    then raise BadFrac
    else if y < 0
    then Frac(~x, ~y)
    else Frac(x,y)

fun add (r1,r2) =
    case (r1,r2) of
        (Whole(i),Whole(j)) => Whole(i+j)
      | (Whole(i),Frac(j,k)) => Frac(j+k*i,k)
      | (Frac(j,k),Whole(i)) => Frac(j+k*i,k)
      | (Frac(a,b),Frac(c,d)) => Frac(a*d+b*c,b*d)          

fun toString r =
    let fun gcd (x,y) =
        if x=y
        then x
        else if x < y
        then gcd(x,y-x)
        else gcd(y,x)

        fun reduce r =
            case r of
                Whole _ => r
              | Frac(x,y) => if x=0
                             then Whole 0
                             else let val d = gcd(abs x, y)
                                  in
                                      if d=y
                                      then Whole(x div d)
                                      else Frac(x div d, y div d)
                                  end
    in
        case reduce r of
                Whole i => Int.toString i
              | Frac(a,b) => (Int.toString a) ^ "/" ^ (Int.toString b)
    end
end;    

上面是另一种实现，gcd函数和reduce函数可以放在最后的toString函数中，假设Rational2和Rational1都使用RATIONAL_A，两者的type-check都会通过，但是结果仍然可能不同，Rational2是最后reduce，因此即便直接通过Frac创建变量，也会输出化简形式，而Rational1不行

  
- Rational1.toString(Rational1.Frac(21,3));
val it = "21/3" : string
- Rational2.toString(Rational2.Frac(21,3));
val it = "7" : string

RATIONAL_A定义了数据类型rational，因此虽然Rational1和Rational2实现有不同，但是仍然需要保持一些invariants，而RATIONAL_B和RATIONAL_C不需要，比如定义一个Rational3，其中rational类型为int * int。Rational3中的Whole函数类型为'a -> 'a * int，RATIONAL_C中的val Whole: int -> rational，两者的类型也能匹配上，前者比后者更通用

  
structure Rational3 :> RATIONAL_C =
struct
type rational = int * int
exception BadFrac

fun make_frac (x,y) =
    if y = 0
    then raise BadFrac
    else if y < 0
    then (~x, ~y)
    else (x,y)

fun Whole i = (i,1)

fun add ((a,b),(c,d)) = (a*d + c*d, b*d)         

fun toString (x,y) =
    if x = 0
    then "0"
    else
    let fun gcd (x,y) =
        if x=y
        then x
        else if x < y
        then gcd(x,y-x)
        else gcd(y,x)
        val d = gcd (abs x, y)
        val num = x div d
        val denom = y div d
    in
        Int.toString num ^ (if denom =1
                then ""
                else "/" ^ (Int.toString denom))
    end
end;

即便不同structure使用相同的signature，不同structure里的bindings不能相互使用

  
- Rational1.toString(Rational2.make_frac(2,3));
stdIn:8.1-8.45 Error: operator and operand do not agree [tycon mismatch]
  operator domain: Rational1.rational
  operand:         Rational2.rational
  in expression:
    Rational1.toString (Rational2.make_frac (2,3))

9.motivating and defining equivalence

通过严格的接口，可以提供不用的等价实现，因为对于客户来说没有区别。等价实现在很多场景下需要用到：

代码维护：是否能更简化，重构代码，但是不会改变剩余代码的行为
可扩展性：可以在代码中增加新的特征，但是不会影响已经存在的特征
优化：可以用一个内存和耗时更优的方式来代替原先实现
抽象：保证对代码做了改动之后不会影响外部用户的使用

那么如何判断两种实现是等价的？

（1）函数f和函数g在任何程序任何输入参数下都有相同的结果和副作用

（2）等价并不意味着要求运行时间一样，或者要求使用到的局部函数或者数据一样，实现细节不同不影响等价性

更具体的等价表现为

产出相同的结果
有相同的终止条件
相同的输入下相同的输出
触发相同的异常
用相同的方式占用内存

10.standard equivalences

等价性中要求任何两段实现都有相同的副作用，ML鼓励程序里不要出现任何副作用，即纯函数式语言pure functional languages，在函数内不要产生可变性。由于可变性的存在，下面两个代码可能结果就不同，前者先执行的f(x)，而后者先执行的g(y)

  
int a = f(x);
int b = g(y);
return b - a;

return g(y) - f(x);

等价性是比较微妙的，必须要求任何被调用的地方都等价，下面是一些等价的经验法则和常见的等价函数

（1）各种形式的语法糖

  
fun f x =
    if x
    then g x
    else false;

fun f x =
    x andalso g x;

（2）可修改的局部变量名称

  
val y = 4;
fun g z = (z+y+z) + z;

val y = 4;
fun f z = z+y+z;

（3）局部函数的使用：有些场景下等价，有些场景下不等价

  
val y = 4;
fun f x = x+y+z;
fun g z = (f z)+z;

（4）匿名函数的使用

  
fun g y = f y;
val g = y;

（5）其他

  
let val p = e1 in e2 end
(fn p => e2) e1.

等价性里不要求运行时间相同，实际上等价实现会有不同的时间复杂度，常在算法使用中用来优化代码。

Coursera, ProgrammingLanguage

programming

This post is licensed under CC BY 4.0 by the author.