https://zhuanlan.zhihu.com/p/84634204
如何类型化一场技术面试
等
原文https://aphyr.com/posts/342-typing-the-technical-interview
草稿，没加译注，欢迎校对
在很久，很久以前，比基督信仰的存在还要早的时候，在那些无定形的旧日时光里，所有的咒语都是由纯粹的因果关系所编织而成的，所有的行为都是被允许的，而死亡是司空见惯的。在那时，许多女巫被她们自己失控的法术所毁灭：人们常常见到，她们支离破碎的躯体躺在一个由扭曲的、被结晶侵蚀的树木和在池水中不断燃烧的石头组成的圆圈的中心。另一些人则完全消失了，或者说，她们在沿着虚无的无尽山脊漫步：她们的脚再也无法触碰地面，她们的呼吸再也无法温暖空气。
你在孩提时代便听闻了古尔薇格[1]的故事，她曾三次重生于对她的审判之火，她曾周游世界表演Seiðr魔术：一种预知并重新编织未来的技艺。她的预言(有很多)是非常著名的-甚至那些超越世界的传奇女巫Völva[2]们也曾提起过-但是真正改变历史的，是她的永生。在Seiðr魔术带来的的狂喜恍惚和谵妄之间，她预见了自己的命运，并征服了死亡。她的咒语永远不会崩溃，她是为社会所不容之人-你这类人的前辈-们的朋友。据说连奥丁本人也是从她那里学到了不老不死的秘密。
直到今天，所有的女巫都欠古尔薇格一笔债。现在很少有人深入研究古代的、非结构化的魔法。今日你用来写下咒语的语言，都是在语法层面稳定的。这些语言通过(或多或少地)安全的途径来引导你所召唤的能量。当然，爆炸偶尔也会发生。但这些事故只是…那种会燎到你的眉毛的类型，而不是那种，会摧毁大地并创造出一些新的，形状有趣的峡湾的类型。
“一切都顺利吗？你还好吗？”
面试官(他的胸牌上写着他的名字，“克里斯”)很年轻，这是硅谷的惯例。他穿着连帽衫，从在衣服上找不到品牌logo这一点来看，这件衣服至少值三百美元。他不像是那种会让你不知所措的类型，你觉得你会处理好这场面试的。
“一般来说？我不这么认为。“你环顾会议室，好像在确认这个世界是否在正常运转。房间的墙壁散发着slack私聊和试图回避矛盾的气息。
“啊，好吧，嗯。是的，可能是吧。“他听起来很害羞。“但是还是让我们来做一道小题。只是一个简单的算法题，让我了解一下你是如何解决难题的。“
有一次，你用一把碎玻璃做的小刀解决了一个难题。你期待着克里斯是否有能力去做你已经做到过的事情。
“所以说…这个问题叫做N-皇后，它相当简单。给定一个NxN棋盘，你需要找到一种方法，将N个皇后安全地放在那个棋盘上。“
你在白板上画了一个8×8的网格，并在中心将八个皇后整齐地排列在一起。她们面对面围成一个紧密的圆圈，平等地交谈。
“呃，不-那是不对的。看这里，这个皇后可以一步移动吃掉这四个中的任何一个“。
“你真的无法想象，”你的声音如同岩石般冷静，“想象八个强悍的女人待在一个房间里，而她们没有开始自相残杀吗？”
“呃…反正问题就是这么问的“
那么，也许她们是正在互相交战的氏族的首领。在一起讨论停战协定，但没有人能够在短剑的攻击范围内相信其他人-这种情形在你们族人的历史上也发生过。
“我可以使用任何编程语言来写这道题吗？”
“当然可以。”
赶快行动，在他意识到自己犯下何种大错之前。
{-# OPTIONS_GHC -fno-warn-missing-methods #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}“哦，这是Haskell！我在大学里学过这个！“他停顿了一下，皱起了眉头。“UndecidableInstances？”
“我们必须用这个扩展，”你兴高采烈地告诉他，“因为Hask不是一个范畴。”
“哦，好吧。”他虚张声势地说了一句没有针对性的开放观点，“这就是我们通常认为Haskell的子集中的类型没有底值的原因。”
“没错。”你小声附和，但是心里并不这么想。虽然面试官没听到。
nil = undefined一个令人不安的问题随着你脑海中浮现的第一件事脱口而出，“为了存储皇后的位置，我们需要某种链表，对吗？”
“当然可以，也可以是Vector。”
“列表更简单。”
“好的，当然。都行。“
你从虚空中召来一个链表。它漂浮在屏幕的表面：一个永恒的结构，能够以一千种方式表达，但总是美妙的。你心满意足地叹了口气。
data Nil
data Cons x xs“你不用标准库吗？”克里斯问，他皱着眉头。
“什么？”你根本不知道他在说什么。“哦，不-我不想import外部库。我觉得手动定义更简单。“
class First list x | list -> x instance First Nil Nil instance First (Cons x more) x“我用class关键字定义了一个函数签名，”你提醒克里斯，他看起来很迷茫。“首先获取列表并从中返回一个值x。我们的函数有两个实现-Haskell使用模式匹配来决定调用哪个。传一个Nil列表给First会返回Nil，传一个Cons则会返回这个列表单元对象里面装的值“
你确保他理解了这一点，然后将两个列表连接在一起。
class ListConcat a b c | a b -> c instance ListConcat Nil x x instance (ListConcat as bs cs) => ListConcat (Cons a as) bs (Cons a cs)“这个箭头是啥？”克里斯问。你告诉他这意味着实质蕴涵。要得到箭头后面的ListConcat，我们需要箭头之前的那个ListConcat。
他灵光一闪，“哦，对！这是递归，因为第二个ListConcat的实现里也出现了ListConcat。第一个有Nil的实现是base case。“
“没错。”你为克里斯感到骄傲，他跟上了。“底下的那个实现是当我们想连接列表时的一般情况。”
-- Concatenate all lists in a list
class ListConcatAll ls l | ls -> l instance ListConcatAll Nil Nil instance (ListConcat chunk acc result, ListConcatAll rest acc) => ListConcatAll (Cons chunk rest) result -- Is any element of this list True? class AnyTrue list t | list -> t instance AnyTrue Nil False instance AnyTrue (Cons True more) True instance (AnyTrue list t) => AnyTrue (Cons False list) t思考这个问题需要比你预期的更多的注意力，所以你准备退回到一些更容易的事情上。 “让我们定义一下布尔代数。”你建议，就像邀请他共进午餐一样。
“为什么？”
“当然是因为我们需要。”
你从虚空中抓住两个无意义的常数，然后赋予它们意义。
data True
data False
class Not b1 b | b1 -> b instance Not False True instance Not True False class Or b1 b2 b | b1 b2 -> b instance Or True True True instance Or True False True instance Or False True True instance Or False False False弗蕾雅女神[4]会很高兴的。一个代数系统降生到这个世界上是一件美妙的事情。
“我想我们也需要整数系统，来表达皇后的位置。”你喃喃地说，“我们只用得到正整数坐标，所以普通的皮亚诺构造应该足够了。” 你从头上拔下一根头发，打了一个首尾相连的结。零。
data Z
data S n type N0 = Z type N1 = S N0 type N2 = S N1 type N3 = S N2 type N4 = S N3 type N5 = S N4 type N6 = S N5 type N7 = S N6 type N8 = S N7“你在…手动定义自然数？为什么要这么做？“
“Haskell是给数学家设计的，”你解释道。“我们总是自己定义东西。”
-- Equality
class PeanoEqual a b t | a b -> t instance PeanoEqual Z Z True instance PeanoEqual (S a) Z False instance PeanoEqual Z (S b) False instance (PeanoEqual a b t) => PeanoEqual (S a) (S b) t -- Comparison (<) class PeanoLT a b t | a b -> t instance PeanoLT Z Z False instance PeanoLT (S x) Z False instance PeanoLT Z (S x) True instance (PeanoLT a b t) => PeanoLT (S a) (S b) t -- Absolute difference class PeanoAbsDiff a b c | a b -> c instance PeanoAbsDiff Z Z Z instance PeanoAbsDiff Z (S b) (S b) instance PeanoAbsDiff (S a) Z (S a) instance (PeanoAbsDiff a b c) => PeanoAbsDiff (S a) (S b) c -- Integers from n to 0 class Range n xs | n -> xs instance Range Z Nil instance (Range n xs) => Range (S n) (Cons n xs)“等等，停一下，”克里斯打断了我。“你不应该…这里不应该有类型声明吗？至少在我们的函数上？“。
你和蔼的微笑，”Haskell是一种动态类型的解释型语言。“
克里斯看起来好像活吞了一只青蛙。
“我给你演示一下，让我们检查一下一是否等于一。“
class LegalCompare t | -> t where legalCompare :: t instance (PeanoEqual (S Z) (S Z) t) => LegalCompare t *Main> :type legalCompare legalCompare :: True“看见没？legalCompare就是True。现在让我们试着写一个执行无效比较的表达式。比如，将True和一个列表进行比较。“
class IllegalCompare t | -> t where illegalCompare :: t instance (PeanoEqual True (Cons Z False) t) => IllegalCompare t“看，你可以把它加载进去。只有当你试图对它求值时，它才会崩溃-记住，Haskell是惰性的。“
*Main> :type illegalCompare illegalCompare :: PeanoEqual True (Cons Z False) t => t“跑一下试试。看！一个运行时类型错误。“。
“这哪里报错了吗…”
“嗯，你知道的。Haskell的错误消息是出了名的难以理解。”
克里斯看起来很难受。你抓住这个机会继续开始实现高阶函数。
“不幸的是，Haskell没有柯里化，所以我们不得不自己整一个实现partial function的机制。这是通用的单参数函数调用的签名。“
class Apply f a r | f a -> r“这只是一个接受输入a并返回r的函数f。”
这些变量有着可爱的如歌般的旋律。
“对于partial function，我们可以定义像Partial1、Partial2之类的数据类型，但由于我们只需要其中的几个，所以直接定义我们需要的那些函数的显式柯里化版本会更容易。像这样。“
data Conj1 list
instance Apply (Conj1 list) x (Cons x list)你深吸了一口气，准备将你的精神体从这些具体的形式中解脱出来，提升到高阶函数的层面。
-- Map f over a list
class Map f xs ys | f xs -> ys instance Map f Nil Nil instance (Apply f x y, Map f xs ys) => Map f (Cons x xs) (Cons y ys) -- Map f over list and concatenate results together class MapCat f xs zs | f xs -> zs instance MapCat f Nil Nil instance (Map f xs chunks, ListConcatAll chunks ys) => MapCat f xs ys -- Filter a list with an Apply-able predicate function class AppendIf pred x ys zs | pred x ys -> zs instance AppendIf True x ys (Cons x ys) instance AppendIf False x ys ys class Filter f xs ys | f xs -> ys instance Filter f Nil Nil instance (Apply f x t, Filter f xs ys, AppendIf t x ys zs) => Filter f (Cons x xs) zs先暂时回到具体值的世界一小会。克里斯还在这里，至少物理上还在这里。由于抽象世界的深沉寒冷，你的笔记本电脑屏幕已经变成了华丽的不同紫色色块(指关键字高亮)的混合，但代码依然隐约可见。它让你想起黄昏时结冰的湖。
液态的结晶。
“克里斯。克里斯。“他快速眨着眼睛，好像刚从黑暗中走出来。好漂亮的眼睛。你想起了你的双眼仍然有颜色的时候。“我们准备好了”
“是的…“。
“皇后是由她在棋盘上的两个坐标定义的：x和y。我们还将构建一个部分求值的构造函数，用于从给定的单独x坐标构造皇后。”
data Queen x y
data Queen1 x instance Apply (Queen1 x) y (Queen x y) -- A list of queens in row x with y from 0 to n. class QueensInRow n x queens | n x -> queens instance (Range n ys, Map (Queen1 x) ys queens) => QueensInRow n x queens“终于来了，皇后！”你喃喃自语。遗憾的是，这不是那种面试。
这些皇后可以朝八个方向侵攻。你一直以为那不过是个隐喻。
-- Does queen a threaten queen b?
class Threatens a b t | a b -> t instance (PeanoEqual ax bx xeq, PeanoEqual ay by yeq, Or xeq yeq xyeq, PeanoAbsDiff ax bx dx, PeanoAbsDiff ay by dy, PeanoEqual dx dy deq, Or xyeq deq res) => Threatens (Queen ax ay) (Queen bx by) res -- Partial application of Threatens data Threatens1 a instance (Threatens a b t) => Apply (Threatens1 a) b t新的一名女皇进入棋盘，昂首阔步地走进了自己的位置。她警觉地看着她的对手们，小心地保持在安全距离。她能站在哪里？你设想了一堆宇宙-不同的世界，每个世界里皇后们都在不同的地方。
-- Is queen b compatible with all queen as?
class Safe config queen t | config queen -> t instance (Map (Threatens1 queen) config m1, AnyTrue m1 t1, Not t1 t2) => Safe config queen t2 data Safe1 config instance (Safe config queen t) => Apply (Safe1 config) queen t -- Add a queen with the given x coordinate to a legal configuration, returning -- a set of legal configurations. class AddQueen n x c cs | n x c -> cs instance (QueensInRow n x candidates, Filter (Safe1 c) candidates filtered, Map (Conj1 c) filtered cs) => AddQueen n x c cs data AddQueen2 n x instance (AddQueen n x c cs) => Apply (AddQueen2 n x) c cs -- Add a queen at x to every configuration, returning a set of legal -- configurations. class AddQueenToAll n x cs cs' | n x cs -> cs' instance (MapCat (AddQueen2 n x) cs cs') => AddQueenToAll n x cs cs'“现在，让万物归于正轨。”你悄声低语，然后将咒语循环给它自己，并用控制流之线将一切缝合。
每行一个皇后，在每个合法的位置，对于每个可能的布局。你可以想象在她们start-up公司官网上的“关于我们”页面会是什么样子。
-- Add queens recursively
class AddQueensIf pred n x cs cs' | pred n x cs -> cs' instance AddQueensIf False n x cs cs instance (AddQueenToAll n x cs cs2, AddQueens n (S x) cs2 cs') => AddQueensIf True n x cs cs' class AddQueens n x cs cs' | n x cs -> cs' instance (PeanoLT x n pred, AddQueensIf pred n x cs cs') => AddQueens n x cs cs' -- Solve class Solution n c | n -> c where solution :: n -> c instance (AddQueens n Z (Cons Nil Nil) cs, First cs c) => Solution n c where solution = nil克里斯看起来已经适应了从荒古而来的遥远凝视。你轻轻地扶着他的肩膀。
“嘘！”你低声说。“万事俱备，答案就在眼前。”
*Main> :type solution (nil :: N6) solution (nil :: N6) :: Cons (Queen (S (S (S (S (S Z))))) (S Z)) (Cons (Queen (S (S (S (S Z)))) (S (S (S Z)))) (Cons (Queen (S (S (S Z))) (S (S (S (S (S Z)))))) (Cons (Queen (S (S Z)) Z) (Cons (Queen (S Z) (S (S Z))) (Cons (Queen Z (S (S (S (S Z))))) Nil)))))看！我们漂亮的标准输出格式就是这样对齐的，沿垂直轴创建了一条可爱的零线。
“所以，皇后的位置在(5,1), (4,3), (3,5), (2,0), (1,2)和(0,4)。这样可以吗，克里斯？”
克里斯盯了你好一会。“你从来没有…你从来没有写过具体值。你…你应该知道类型系统只是用来约束值的，对吧？“
“不。”你实事求是地告诉他。“不，不是这样的。”
他向后靠在椅子上-你担心他可能会摔倒-然后将整张脸埋进了双手。
你，通过Seiðr魔术，已经清晰地看到了你的拒信，并且知道他将要在拒信上写些什么。
“我们会保持联系的。”
衷心感谢Patrick Thomson和Conrad Parker的Type Level Instant Insanity
原文地址：http://www.cnblogs.com/OURS2025/p/16899132.html
