PPL Lab3

实验要求

请在实验前阅读本文件, 以免错过重要信息. 在本实验中, 你将使用 OCaml 实现一个完整的 Hindley-Milner 类型推导算法. 原则上, 代码文件中的注释足以帮助你完成实验, 如有问题, 请联系我们.

项目结构

lib/ 下的文件:

• info.ml 你的个人信息 应该 填写在此处.
• infer.ml 你应该在这里完成所有的类型推导实验内容
• syntax.ml 你可以通过查看这个文件来熟悉本次我们使用的语言 这个文件还包含很多你可能会用到的打印函数
• type.ml 你可以通过查看这个文件了解本次实验中我们关心的一些结构 这个文件还包含很多你可能会用到的打印函数
• fresh.ml 用于产生新的类型变量
• util.ml 包含两个实用的运算符，可以将字符串方便的转为类型或者表达式
• token.mly lexer.mll parser.mly typeparser.mly display.ml 这是助教为你提供的帮助函数库, 你不需要关心这一部分的代码实现. 若有需要, 你只需阅读函数名, 并借助 dune utop 来查看对应函数的类型.

实验组成

实验分为两部分, 其中后一部分依赖前一部分:

1. 简单的类型推导, infer.ml:Infer_no_let
2. 完整的带有 let polymorphism 的 HM 类型推导 infer.ml:Infer

仅就实验指导而言, 你应当按如下顺序阅读文件中的注释:

1. info.ml 填写个人信息
2. syntax.ml 了解 term 的语法结构
3. type.ml 了解 type, substitution, constr, type scheme, context 的结构
4. infer.ml 实现类型推导

调试指南

本次实验中，你可以使用 dune exec lab3 或 dune test 来分别以 bin/main.ml 或 test/test.ml 为入口执行内容。如果你想使用 OCaml Debugger，那么建议使用前者。

print 法

本次实验提供了大量辅助用的 pretty printer 函数，所以可以有很好的调试效果。这些函数分为两大类，print_* 类直接向 stdout 进行输出并返回 unit 类型；show_* 类则返回一个 string。 具体而言，你可以直接使用

• *_ty: 以自然的格式打印一个类型
• *_constr: 以自然的格式打印一个类型约束
• *_subst: 以自然的格式打印一个类型替换
• *_constrs: 以自然的格式打印类型约束列表
• *_substs: 以自然的格式打印类型替换列表
• *_expr: 以自然的格式打印一个表达式（其中 lambda abstraction 显示为 \x. e 形式）
• *_expr_in_ocaml: 以自然的格式打印一个表达式（其中 lambda abstraction 显示为 fun x -> e 形式）。如果你不确定一个 expr 的类型，你可以使用这个打印函数，将 expr 的文本形式输入 utop 并借助 OCaml 的类型推导器来帮你找出正确的类型。

debugger 法

此处不提供具体的 OCaml Debugger 使用方法，可以查看这儿的帮助内容。到目前为止，OCaml Debugger 也没有与 IDE 和 VSCode 的集成插件，所以也不能完全称得上好用。 为了你方便使用 ocamldebug，lab-3 的 bin 部分打开了字节码模式（来防止 dune 对于部分函数符号的修饰）。在你 dune build 后，你应该通过 ocamldebug _build/default/bin/main.bc 命令来开始调试。

分数组成

共有 50 个测试点，每个 2 分， 其中第一部分有 37 个测试点， 第二部分 13 个测试点。 带有 (+) 前缀的为正向测试点，在这些测试点中，你需要推导出一个正确的类型。 带有 (-) 前缀的为反向测试点，在这些测试点中，你需要抛出异常。具体请见 infer.ml。

Experiment requirements

Please read this document before writing any code so you will not miss important information.

In this lab, you will implement a Hindley-Milner type inference algorithm in OCaml. The comments in the code file are enough to help you complete the experiment, if you have any questions, please contact us.

Project structure

Files under lib/:

• info.ml You should put your personal information here.
• infer.ml You should implement a Hindley-Milner type inference algorithm here.
• syntax.ml You can familiarize yourself with the language we use this time by looking at this file This file also contains many printing functions that you can use.
• type.ml You can see some of the structures we care about in this experiment by looking at this file This file also contains many printing functions that you can use.
• fresh.ml Used to generate new type variables.
• util.ml Contains two practical operators that can easily convert strings to types or expressions.
• token.mly lexer.mll parser.mly typeparser.mly display.ml This is the helper function library provided by the TA, you don't need to care about the implementation of this part of the code. If necessary, you can read the function name and use dune utop to see the type of the corresponding function.

What to do

The experiment has two parts, where the latter part depends on the former part:

1. Simple type inference, infer.ml:Infer_no_let
2. Complete HM type inference with let polymorphism infer.ml:Infer

For lab instructions only, you should read the notes in the file in the following order:

1. info.ml fill in personal information
2. syntax.ml understands the grammar of term
3. type.ml understands the structure of type, substitution, consstr, type scheme, context
4. infer.ml implements type inference algorithm

How to debug

In this experiment, you can use dune exec lab3 or dune test to execute bin/main.ml or test/test.ml as the entry point respectively. If you want to use OCaml Debugger, the former is recommended.

Pretty print functions

This experiment provides a lot of auxiliary pretty print functions, which may help your debugging. These functions are in two categories, the print_* functions directly outputs to stdout and returns the unit type; the show_* functions returns a string. Specifically, you can directly use

• *_ty: print a type in its human-readable format
• *_constr: print a type constraint in human-readable format
• *_subst: print a type substitution in human-readable format
• *_constrs: print list of type constraints in human-readable format
• *_substs: print list of type substitutions in human-readable format
• *_expr: print an expression in human-readable format (where lambda abstraction is shown as \x.e)
• *_expr_in_ocaml: print an expression in human-readable format (where lambda abstraction appears as fun x -> e). If you're not sure about the type of an expr, you can use the print function, which put the string of expr into utop and uses OCaml's type inference to help you figure out the correct type.

OCaml Debugger

The specific usage method of OCaml Debugger is not provided here, you can check the help content here. For now, OCaml Debugger has no integrated plug-ins with IDE or VSCode, so it is not convenient to use. For your convenience to use ocamldebug, we enabled the bytecode mode (to prevent dune from modifying some function symbols) in the bin part of lab-3 . After you dune build, you can start debugging with the ocamldebug _build/default/bin/main.bc command.

Scoring details

There are 50 test cases, you get 2 points after passing each test case. The first part has 37 test cases. The second part has 13 test cases. The test cases prefixed with (+) are positive cases where you need to infer a correct type. The test cases prefixed with (-) are negative cases where you need to throw an exception. See infer.ml for details.