「SF-QC」2 TypeClasses - 黄玄的博客

Considerring printing different types with this common idiom:

1
2
3
4
5
6



showBool : bool → string
showNat : nat → string
showList : {A : Type} (A → string) → (list A) → string
showPair : {A B : Type} (A → string) → (B → string) → A * B → string

Definition showListOfPairsOfNats := showList (showPair showNat showNat)   (* LOL *)

The designers of Haskell addressed this clunkiness through typeclasses, a mechanism by which the typechecker is instructed to automatically construct “type-driven” functions [Wadler and Blott 1989].

Coq followed Haskell’s lead as well, but

because Coq’s type system is so much richer than that of Haskell, and because typeclasses in Coq are used to automatically construct not only programs but also proofs, Coq’s presentation of typeclasses is quite a bit less “transparent”

Basics

Classes and Instances

1
2
3
4
5
6
7



Class Show A : Type := {
  show : A → string
}.

Instance showBool : Show bool := {
  show := fun b:bool ? if b then "true" else "false"
}.

Comparing with Haskell:

1
2
3
4
5
6



class Show a where
  show :: a -> string

--  you cannot override a `instance` so in reality you need a `newtype` wrapper to do this
instance Show Bool where
  show b = if b then "True" else "Fasle"

The show function is sometimes said to be overloaded, since it can be applied to arguments of many types, with potentially radically different behavior depending on the type of its argument.

Next, we can define functions that use the overloaded function show like this:

1
2
3
4
5
6
7
8
9
10
11
12



Definition showOne {A : Type} `{Show A} (a : A) : string :=
  "The value is " ++ show a.

Compute (showOne true).
Compute (showOne 42).

Definition showTwo {A B : Type}
           `{Show A} `{Show B} (a : A) (b : B) : string :=
  "First is " ++ show a ++ " and second is " ++ show b.

Compute (showTwo true 42).
Compute (showTwo Red Green).

The parameter `{Show A} is a class constraint, which states that the function showOne is expected to be applied only to types A that belong to the Show class.

Concretely, this constraint should be thought of as an extra parameter to showOne supplying evidence that A is an instance of Show — i.e., it is essentially just a show function for A, which is implicitly invoked by the expression show a.

读时猜测（后来发现接下来有更正确的解释）：show 在 name resolution 到 class Show 时就可以根据其参数的 type（比如 T）infer 出「我们需要一个 Show T 的实现（instance，其实就是个 table）」，在 Haskell/Rust 中这个 table 会在 lower 到 IR 时才 made explicit，而 Coq 这里的语法就已经强调了这里需要 implicitly-and-inferred {} 一个 table，这个 table 的名字其实不重要，只要其 type 是被 A parametrized 的 Show 就好了，类似 ML 的 functor 或者 Java 的 generic interface。

This is Ad-hoc polymorphism.

Missing Constraint

What if we forget the class constrints:

1
2
3
4
5
6
7



Error:
Unable to satisfy the following constraints:
In environment:
A : Type
a : A

?Show : "Show A"

Class Eq

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22



Class Eq A :=
  {
    eqb: A → A → bool;
  }.

Notation "x =? y" := (eqb x y) (at level 70).

Instance eqBool : Eq bool :=
  {
    eqb := fun (b c : bool) ?
       match b, c with
         | true, true ? true
         | true, false ? false
         | false, true ? false
         | false, false ? true
       end
  }.

Instance eqNat : Eq nat :=
  {
    eqb := Nat.eqb
  }.

Why should we need to define a typeclass for boolean equality when Coq’s propositional equality (x = y) is completely generic?
while it makes sense to claim that two values x and y are equal no matter what their type is, it is not possible to write a decidable equality checker for arbitrary types. In particular, equality at types like nat → nat is undecidable.

x = y 返回一个需要去证的 Prop (relational) 而非 executable Fixpoint (functional)
因为 function 的 equality 有时候会 undeciable，所以才需要加 Functional Extensionality Axiom（见 LF-06）

1
2
3
4
5
6
7
8
9



Instance eqBoolArrowBool: Eq (bool -> bool) :=
  {
    eqb := fun (f1 f2 : bool -> bool) =>
      (f1 true) =? (f2 true) && (f1 false) =? (f2 false)
  }.

Compute (id =? id).      (* ==> true *)
Compute (negb =? negb).  (* ==> true *)
Compute (id =? negb).    (* ==> false *)

这里这个 eqb 的定义也是基于 extensionality 的定义，如果考虑到 effects（divergence、IO）是很容易 break 的（类似 parametricity）

Parameterized Instances: New Typeclasses from Old

Structural recursion

1
2
3
4
5
6
7



Instance showPair {A B : Type} `{Show A} `{Show B} : Show (A * B) :=
  {
    show p :=
      let (a,b) := p in
        "(" ++ show a ++ "," ++ show b ++ ")"
  }.
Compute (show (true,42)).

Structural equality

1
2
3
4
5
6
7



Instance eqPair {A B : Type} `{Eq A} `{Eq B} : Eq (A * B) :=
  {
    eqb p1 p2 :=
      let (p1a,p1b) := p1 in
      let (p2a,p2b) := p2 in
      andb (p1a =? p2a) (p1b =? p2b)
  }.

Slightly more complicated example: typical list:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24



(* the book didn't use any from ListNotation *)
Fixpoint showListAux {A : Type} (s : A → string) (l : list A) : string :=
  match l with
    | nil ? ""
    | cons h nil ? s h
    | cons h t ? append (append (s h) ", ") (showListAux s t)
  end.
Instance showList {A : Type} `{Show A} : Show (list A) :=
  {
    show l := append "[" (append (showListAux show l) "]")
  }.

(* I used them though *)
Fixpoint eqListAux {A : Type} `{Eq A} (l1 l2 : list A) : bool :=
  match l1, l2 with
    | nil, nil => true
    | (h1::t1), (h2::t2) => (h1 =? h2) && (eqListAux t1 t2)
    | _, _ => false
  end.

Instance eqList {A : Type} `{Eq A} : Eq (list A) :=
  {
    eqb l1 l2 := eqListAux l1 l2
  }.

Class Hierarchies

we might want a typeclass Ord for “ordered types” that support both equality and a less-or-equal comparison operator.

A bad way would be declare a new class with two func eq and le.

It’s better to establish dependencies between typeclasses, similar with OOP class inheritence and subtyping (but better!), this gave good code reuses.

We often want to organize typeclasses into hierarchies.

1
2
3
4
5
6
7
8



Class Ord A `{Eq A} : Type :=
  {
    le : A → A → bool
  }.
Check Ord. (* ==>
Ord
     : forall A : Type, Eq A -> Type
*)

class Eq is a “super(type)class” of Ord (not to be confused with OOP superclass)

This is Sub-typeclassing.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22



Fixpoint listOrdAux {A : Type} `{Ord A} (l1 l2 : list A) : bool :=
  match l1, l2 with
  | [], _ => true
  | _, [] => false
  | h1::t1, h2::t2 => if (h1 =? h2)
                     then (listOrdAux t1 t2)
                     else (le h1 h2)
  end.

Instance listOrd {A : Type} `{Ord A} : Ord (list A) :=
  {
    le l1 l2 := listOrdAux l1 l2
  }.

(* truthy *)
Compute (le [1] [2]).
Compute (le [1;2] [2;2]).
Compute (le [1;2;3] [2]).

(* falsy *)
Compute (le [1;2;3] [1]).
Compute (le [2] [1;2;3]).

How It works

Implicit Generalization

所以 `{...} 这个 “backtick” notation is called implicit generalization，比 implicit {} 多做了一件自动 generalize 泛化 free varabile 的事情。

that was added to Coq to support typeclasses but that can also be used to good effect elsewhere.

1
2
3
4
5
6
7
8
9
10
11



Definition showOne1 `{Show A} (a : A) : string :=
  "The value is " ++ show a.

Print showOne1.
(* ==>
    showOne1 =
      fun (A : Type) (H : Show A) (a : A) => "The value is " ++ show a
           : forall A : Type, Show A -> A -> string

    Arguments A, H are implicit and maximally inserted
*)

notice that the occurrence of A inside the `{...} is unbound and automatically insert the binding that we wrote explicitly before.

The “implicit and maximally generalized” annotation on the last line means that the automatically inserted bindings are treated (注：printed) as if they had been written with {...}, rather than (...).

The “implicit” part means that the type argument A and the Show witness H are usually expected to be left implicit
whenever we write showOne1, Coq will automatically insert two unification variables as the first two arguments.

This automatic insertion can be disabled by writing @, so a bare occurrence of showOne1 means the same as @showOne1 _ _

这里的 witness H 即 A implements Show 的 evidence，本质就是个 table or record，可以 written more explicitly:

1
2
3
4
5



Definition showOne2 `{_ : Show A} (a : A) : string :=
  "The value is " ++ show a.

Definition showOne3 `{H : Show A} (a : A) : string :=
  "The value is " ++ show a.

甚至

1
2



Definition showOne4 `{Show} a : string :=
  "The value is " ++ show a.

1
2
3
4
5
6
7
8
9



showOne =
fun (A : Type) (H : Show A) (a : A) => "The value is " ++ show a
     : forall A : Type, Show A -> A -> string

Set Printing Implicit.

showOne =
fun (A : Type) (H : Show A) (a : A) => "The value is " ++ @show A H a     (* <-- 注意这里 *)
     : forall A : Type, Show A -> A -> string

vs. Haskell

顺便，Haskell 的话，Show 是可以直接 inferred from the use of show 得

1
2
3



Prelude> showOne a = show a
Prelude> :t showOne
showOne :: Show a => a -> String

但是 Coq 不行，会退化上「上一个定义的 instance Show」，还挺奇怪的（

1
2



Definition showOne5 a : string :=  (* not generalized *)
  "The value is " ++ show a.

Free Superclass Instance

``{Ord A} led Coq to fill in both A and H : Eq A because it's the superclass of Ord` (appears as the second argument).

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15



Definition max1 `{Ord A} (x y : A) :=
  if le x y then y else x.

Set Printing Implicit.
Print max1.
(* ==>
     max1 =
       fun (A : Type) (H : Eq A) (H0 : @Ord A H) (x y : A) =>
         if @le A H H0 x y then y else x

   : forall (A : Type) (H : Eq A),
       @Ord A H -> A -> A -> A
*)
Check Ord.
(* ==> Ord : forall A : Type, Eq A -> Type *)

Ord type 写详细的话可以是：

1



Ord : forall (A : Type),大专栏  「SF-QC」2 TypeClasses - 黄玄的博客an class="w">
				


				
时间： 2024-10-27 10:58:38 
		

		


	
	
	

		


		
「SF-QC」2 TypeClasses - 黄玄的博客的相关文章

								

		

			

                黄聪：博客园的积分和排名算法探讨，积分是怎么计算的？（转）
			
		
		

									

				我们先来看看现行规则,用公式表示为:-------------------------------------------------------------------BlogScore = BeRead + 10 * BeComment + 50 * CommentBlogScore:博客积分BeRead:个人博客所有随笔和文章的阅读数之和BeComment:个人博客被评论总数Comment: 个人所发表的评论总数---------------------------------------			
		
	
				

		

			

                深入探究 Function & Object 鸡蛋问题 - 黄庆的博客
			
		
		

									

				引言 这篇文章深入探究下 Function.__proto__ === Function.prototype 引起的鸡生蛋蛋生鸡问题,并在这个过程中深入了解 Object.prototype. Function.prototype. function Object . function Function 之间的关系. Object.prototype Object.prototype 表示 Object 的原型对象,其 [[Prototype]] 属性是 null,访问器属性 __proto__			
		
	
				

		

			

                「专题总结」LCT 2
			
		
		

									

				差不多理解板子之后,写了一些奇怪的题. 但是还是那个问题:树剖真好使. 魔法森林:mikufun说这个是傻逼题. 为了得到书法大家的真传,小 E 同学下定决心去拜访住在魔法森林中的隐士. 魔法森林可以被看成一个包含n个节点m条边的无向图,节点标号为1-n,边标号为1-m. 初始时小 E 同学在号节点 ,隐士则住在n号节点.小 E 需要通过这一片魔法森林,才能够拜访到隐士. 魔法森林中居住了一些妖怪.每当有人经过一条边的时候,这条边上的妖怪就会对其发起攻击. 幸运的是,在1号节点住着两种守护精灵:			
		
	
				

		

			

                怎样将「插件化」接入到项目之中？
			
		
		

									

				本期移动开发精英社群讨论的主题是「插件化」,上网查了一下,发现一篇 CSDN 博主写的文章<Android 使用动态载入框架DL进行插件化开发>.此处引用原作者的话: 随着应用的不断迭代,应用的体积不断增大,项目越来越臃肿,冗余添加.项目新功能的加入,无法确定与用户匹配性,发生严重异常往往牵一发而动全身,仅仅能紧急公布补丁版本号,强制用户进行更新.结果频繁的更新.反而easy减少用户使用黏性,或者是公司业务的不断发展,同系的应用越来越多,传统方式须要通过用户量最大的主项目进行引导下载并安装.			
		
	
				

		

			

                「C语言」常量和变量的表示及应用
			
		
		

									

				先发布,还在修改完善中.. 在程序运行中,其值不能改变的量成为常量.在基本数据类型中,常量可分为整型常量.实型常量.符号常量和字符型常量(包括字符常量和字符串常量),现分别介绍如下: 整型常量 即整常数,由一个或多个数字组成,可以带正负号 C语言中整型常量可用十进制.八进制和十六进制3种形式表示 十进制整数:由0~9数字组成,不能以0开始,没有前缀 八进制整数:以0为前缀,其后由0~7的数字组成,没有小数部分 十六进制整数:以0x或0X开头,其后由0~9的数字和a~f(或A~F字母组成) 另外长			
		
	
				

		

			

                Chrome 扩展 Stylish ：给不喜欢某个网站一键「换肤」
			
		
		

									

				原文地址:http://whosmall.com/?post=419 本文标签: Chrome扩展 Chrome浏览器 Chrome插件 Chrome扩展Stylish Stylish是什么 Stylish 是什么? 开门见山,Stylish 的作用是,它可以把百度首页变成这样: 它还能把知乎「拍扁」,让微博网页版变得简洁无比,让 Feedly 用上Material Design-- 这个神奇的 Stylish实际上是一个浏览器插件,适用于 Chrome,Firefox,Opera 以及 Saf			
		
	
				

		

			

                3D高科技投影　麦可「复活登台」幕后
			
		
		

									

				美国告示牌音乐颁奖典礼,日前在赌城盛大举行,主办单位利用高科技投影技术,让麦可杰克森「复活」登台表演,3D全像投影,加上影片与真人舞群无缝接轨,高科技让过世的大明星彷佛活了过来. 流行乐天王麦可杰克森死而复生,过世将近5年的他,又现身在今年美国告示牌音乐颁奖典礼上,金光闪闪现身舞台中央,麦可杰克森回来了,再现招牌的动感舞步,流露巨星风采,主办单位利用3D全像摄影技术,秘密制作了半年多,把他带回到世人眼前. 特效专家:「观众在告示牌典礼上看到的是,麦可的头部数字影像,连接到一名演员身上,我们实时捕			
		
	
				

		

			

                「Maven Tips」（一）自动更新jar包
			
		
		

									

				maven中手动去更新jar包,是一件比较繁琐麻烦的事情,使用Range Dependency则可以省去这一步骤. 部分jar包可能会自动升级到beat版本! 官方说明文档:Dependency Version Ranges Range Meaning (,1.0] version ≤ 1.0 1.0 固定1.0版本 [1.0]   [1.2,1.3] 1.2 ≤ version ≤ 1.3 [1.0,2.0) 1.0 ≤ version ≤ 2.0 [1.5,) version ≥ 1.5 (			
		
	
				

		

			

                Linux 小知识翻译 - 「桌面环境」
			
		
		

									

				这次聊聊桌面环境. 上次聊了 X Window System 相关的内容,虽然令人意外,但X Window System 和桌面环境不是一回事.请大家稍微考虑一下. X Window System 是指提供GUI环境的软件或者协议.与之相对,「桌面环境」是指工具栏,图标,窗口管理器,桌面管理器等等各式各样软件组合起来的GUI软件包. 换句话说,就是「使用桌面所必需的软件的集合」. 有名的桌面环境有「GNOME」和「KDE」.最近,很多Linux的发行版并不关心使用的桌面环境是「GNOME」还是「			
		
	
	
	

	







      
    
    

    

      

        © 2024 憋错料        | info#biecuoliao.com        | 10 q. 0.022 s.