Polymorphic Perplexion

栏目: IT技术 · 发布时间: 4年前

内容简介:Tags:basicPolymorphism plays a vital role in automating verification in LH. However, thanks to its ubiquity, we often take it for granted, and it can be quite baffling to figure out why verification fails with monomorphic signatures. Let me explain why, us

Tags:basic

Polymorphism plays a vital role in automating verification in LH. However, thanks to its ubiquity, we often take it for granted, and it can be quite baffling to figure out why verification fails with monomorphic signatures. Let me explain why, using a simple example that has puzzled me and other users several times.

22: 
23: module PolymorphicPerplexion where

A Type for Ordered Lists

Previously we have seen how you can use LH to define a type of lists whose values are in increasing (ok, non-decreasing!) order.

First, we define an IncList a type, with Emp (“empty”) and :< (“cons”) constructors.

38: data IncList a = Emp
39:                | (:<) { hd :: a, tl :: IncList a }
40: 
41: infixr 9 :<

Next, we refine the type to specify that each “cons” :< constructor takes as input a hd and a tl which must be an IncList a of values v each of which is greater than hd .

50: {-@ data IncList a = Emp 
51:                    | (:<) { hd :: a, tl :: IncList {v:a | hd <= v}}  
52:   @-}

We can confirm that the above definition ensures that the only legal values are increasingly ordered lists, as LH accepts the first list below, but rejects the second where the elements are out of order.

61: legalList :: IncList Int
62: (PolymorphicPerplexion.IncList GHC.Types.Int)legalList = GHC.Types.Int0 :< GHC.Types.Int1 :< GHC.Types.Int2 :< GHC.Types.Int3 :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp
63: 
64: illegalList :: IncList Int 
65: (PolymorphicPerplexion.IncList GHC.Types.Int)illegalList = GHC.Types.Int0 :< GHC.Types.Int1 :< GHC.Types.Int3 :< GHC.Types.Int2 :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp

A Polymorphic Insertion Sort

Next, lets write a simple insertion-sort function that takes a plain unordered list of [a] and returns the elements in increasing order:

76: insertSortP :: (Ord a) => [a] -> IncList a
77: forall a .
(GHC.Classes.Ord<[]> a) =>
[a] -> (PolymorphicPerplexion.IncList a)insertSortP [a]xs = foldr a -> (PolymorphicPerplexion.IncList a) -> (PolymorphicPerplexion.IncList a)insertP {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp {v : [a] | len v >= 0
           && v == xs}xs
78: 
79: insertP             :: (Ord a) => a -> IncList a -> IncList a
80: forall a .
(GHC.Classes.Ord<[]> a) =>
a -> (PolymorphicPerplexion.IncList a) -> (PolymorphicPerplexion.IncList a)insertP ay Emp       = {VV : a | VV == y}y :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp
81: insertP y (x :< xs)
82:   | {VV : a | VV == y}y <= {VV : a | VV == x}x         = {VV : a | VV == y}y :< {VV : a | VV == x}x :< {v : (PolymorphicPerplexion.IncList {VV : a | x <= VV}) | v == xs}xs
83:   | otherwise      = {VV : a | VV == x}x :< (PolymorphicPerplexion.IncList a)insertP {VV : a | VV == y}y {v : (PolymorphicPerplexion.IncList {VV : a | x <= VV}) | v == xs}xs

Happily, LH is able to verify the above code without any trouble! (If that seemed too easy, don’t worry: if you mess up the comparison, e.g. change the guard to x <= y LH will complain about it.)

A Monomorphic Insertion Sort

However, lets take the exact same code as above but change the type signatures to make the functions monomorphic , here, specialized to Int lists.

99: insertSortM :: [Int] -> IncList Int 
100: [GHC.Types.Int] -> (PolymorphicPerplexion.IncList GHC.Types.Int)insertSortM [GHC.Types.Int]xs = foldr GHC.Types.Int -> (PolymorphicPerplexion.IncList GHC.Types.Int) -> (PolymorphicPerplexion.IncList GHC.Types.Int)insertM {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp {v : [GHC.Types.Int] | len v >= 0
                       && v == xs}xs
101: 
102: insertM            :: Int -> IncList Int -> IncList Int 
103: GHC.Types.Int -> (PolymorphicPerplexion.IncList GHC.Types.Int) -> (PolymorphicPerplexion.IncList GHC.Types.Int)insertM GHC.Types.Inty Emp      = {v : GHC.Types.Int | v == y}y :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp
104: insertM y (x :< xs)
105:   | {v : GHC.Types.Int | v == y}y <= {v : GHC.Types.Int | v == x}x         = {v : GHC.Types.Int | v == y}y :< {v : GHC.Types.Int | v == x}x :< {v : (PolymorphicPerplexion.IncList {v : GHC.Types.Int | x <= v}) | v == xs}xs
106:   | otherwise      = {v : GHC.Types.Int | v == x}x :< (PolymorphicPerplexion.IncList GHC.Types.Int)insertM {v : GHC.Types.Int | v == y}y {v : (PolymorphicPerplexion.IncList {v : GHC.Types.Int | x <= v}) | v == xs}xs

Huh? Now LH appears to be unhappy with the code! How is this possible?

Lets look at the type error:

114:  /Users/rjhala/PerplexingPolymorphicProperties.lhs:80:27-38: Error: Liquid Type Mismatch
115:   
116:  80 |   | otherwise      = x :< insertM y xs
117:                                 ^^^^^^^^^^^^
118:    Inferred type
119:      VV : Int
120:   
121:    not a subtype of Required type
122:      VV : {VV : Int | x <= VV}
123:   
124:    In Context
125:      x : Int

LH expects that since we’re using the “cons” operator :< the “tail” value insertM y xs must contain values VV that are greater than the “head” x . The error says that, LH cannot prove this requirement of actual list insertM y xs .

Hmm, well thats a puzzler. Two questions that should come to mind.

  1. Why does the above fact hold in the first place?

  2. How is LH able to deduce this fact with the polymorphic signature but not the monomorphic one?

Lets ponder the first question: why is every element of insert y xs in fact larger than x ? For three reasons:

  1. every element in xs is larger than x , as the list x :< xs was ordered,

  2. y is larger than x as established by the otherwise and crucially

  3. the elements returned by insert y xs are either y or from xs !

Now onto the second question: how does LH verify the polymorphic code, but not the monomorphic one? The reason is the fact (c)! LH is a modular verifier, meaning that the only information that it has about the behavior of insert at a call-site is the information captured in the (refinement) type specification for insert . The polymorphic signature:

156: insertP :: (Ord a) => a -> IncList a -> IncList a

via parametricity , implicitly states fact (c). That is, if at a call-site insertP y xs we pass in a value that is greater an x and a list of values greater than x then via polymorphic instantiation at the call-site, LH infers that the returned value must also be a list of elements greater than x !

However, the monomorphic signature

167: insertM :: Int -> IncList Int -> IncList Int

offers no such insight. It simply says the function takes in an Int and another ordered list of Int and returns another ordered list, whose actual elements could be arbitrary Int . Specifically, at the call-site insertP y xs LH has no way to conclude the the returned elements are indeed greater than x and hence rejects the monomorphic code.

Perplexity

While parametricity is all very nice, and LH’s polymorphic instanatiation is very clever and useful, it can also be quite mysterious. For example, q curious user Oisín pointed out that while the code below is rejected that if you uncomment the type signature for go then it is accepted by LH!

187: insertSortP' :: (Ord a) => [a] -> IncList a 
188: forall a .
(GHC.Classes.Ord<[]> a) =>
[a] -> (PolymorphicPerplexion.IncList a)insertSortP' = (PolymorphicPerplexion.IncList a)foldr a -> (PolymorphicPerplexion.IncList a) -> (PolymorphicPerplexion.IncList a)go {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp 
189:   where
190:     -- go :: (Ord a) => a -> IncList a -> IncList a
191:     a -> (PolymorphicPerplexion.IncList a) -> (PolymorphicPerplexion.IncList a)go ay Emp       = {VV : a | VV == y}y :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp
192:     go y (x :< xs)
193:       | {VV : a | VV == y}y <= {VV : a | VV == x}x     = {VV : a | VV == y}y :< {VV : a | VV == x}x :< {v : (PolymorphicPerplexion.IncList {VV : a | x <= VV}) | v == xs}xs
194:       | otherwise  = {VV : a | VV == x}x :< (PolymorphicPerplexion.IncList a)go {VV : a | VV == y}y {v : (PolymorphicPerplexion.IncList {VV : a | x <= VV}) | v == xs}xs

This is thoroughly perplexing, but again, is explained by the absence of parametricity. When we remove the type signature, GHC defaults to giving go a monomorphic signature where the a is not universally quantified, and which roughly captures the same specification as the monomorphic insertM above causing verification to fail!

Restoring the signature provides LH with the polymorphic specification, which can be instantiated at the call-site to recover the fact (c) that is crucial for verification.

Moral

I hope that example illustrates two points.

First, parametric polymorphism lets type specifications say a lot more than they immediately let on: so do write polymorphic signatures whenever possible.

Second, on a less happy note, explaining why fancy type checkers fail remains a vexing problem, whose difficulty is compounded by increasing the cleverness of the type system.

We’d love to hear any ideas you might have to solve the explanation problem!


以上就是本文的全部内容,希望对大家的学习有所帮助,也希望大家多多支持 码农网

查看所有标签

猜你喜欢:

本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们

首席增长官

首席增长官

张溪梦 / 机械工业出版社 / 2017-11-1 / 69.9

增长是企业永恒的主题,是商业的本质。 人口红利和流量红利的窗口期正在关闭,曾经“流量为王”所带来的成功经验正在失效,所造成的思维逻辑和方法论亟待更新。在互联网下半场,企业要如何保持增长?传统企业是否能跟上数字化转型的脚步,找到新兴业务的增长模式?为什么可口可乐公司用首席增长官取代了首席营销官职位? 数据驱动增长正在成为企业发展的必需理念,首席增长官、增长团队和增长黑客将是未来商业的趋势......一起来看看 《首席增长官》 这本书的介绍吧!

JSON 在线解析
JSON 在线解析

在线 JSON 格式化工具

RGB转16进制工具
RGB转16进制工具

RGB HEX 互转工具

在线进制转换器
在线进制转换器

各进制数互转换器