{"id":12168,"date":"2015-09-03T10:30:23","date_gmt":"2015-09-03T14:30:23","guid":{"rendered":"http:\/\/mjtsai.com\/blog\/?p=12168"},"modified":"2015-10-04T12:55:42","modified_gmt":"2015-10-04T16:55:42","slug":"why-dependent-types-matter","status":"publish","type":"post","link":"https:\/\/mjtsai.com\/blog\/2015\/09\/03\/why-dependent-types-matter\/","title":{"rendered":"Why Dependent Types Matter"},"content":{"rendered":"

Jeremy W. Sherman<\/a>:<\/p>\n

\n

A dependent type is a type that depends, not just on other types, but on terms. This means you can have values – plain old data – in your types. A common example is that of length-indexed lists.<\/p>\n

You likely caught on that that code is Swift-ish but not actually Swift.\nThat’s DTSwift, where I pretend that Swift is dependently typed.<\/p>\n

[…]<\/p>\n

This means that dependent types give us pay-as-you-go provable correctness. You can require proof of the most critical properties in your program in the form of very specific types that ensure those invariants, while handwaving about components that are either less important or just more readily shown correct by test or inspection.<\/p>\n

[…]<\/p>\n

Dependent types let you replace a Boolean that throws away the knowledge gained from a test by a type that represents the outcome of that test.<\/p>\n<\/blockquote>\n

Update (2015-09-04): Joe Groff<\/a> recommends Certified Programming with Dependent Types<\/a>.<\/p>\n

David Owens II<\/a>:<\/p>\n

This is the part I don’t get: we allow for incorrect code to be written in the non-dependent-typed case, but we assume that we can’t do the same with depedently-typed code? Why? What’s preventing me from swapping left<\/code> and right<\/code> in the Order<\/code> type that is returned?<\/p><\/blockquote>\n

Update (2015-10-04): Jeremy W. Sherman<\/a>:<\/p>\n

\n

Unlike in the evidence-less case, though,\nconsumers of instances of this type can work out that it’s the wrong\nway around based on the because<\/code> evidence:\nan instance like\nlessThanOrEqual(zeroLEQEverything: LEQ(0, 1)): OrderFlippedInstances(1, 0)<\/code>\nhands the consumer a proof that LEQ(0, 1)<\/code>,\nand if they pattern-match that out and use it –\nas they likely would while producing evidence for the correctness of\nwhatever they’re building atop this data –\nit’s merely frustrating that our documentation is backwards.<\/p>\n

This “solves” the flipped Boolean problem,\nbut no tool can solve the problem of misleading names.\nMisleading names provide bad input into our informal reasoning processes,\nand we’re likely to write bogus code as a result.\nIf we’re programming with evidence,\nas dependent types let us do,\nwe’ll catch this while interacting with the compiler;\nif we’re trusting the names,\nand ignoring the evidence,\nas dependent types also let us do\n(and non-dependent types force us to do),\nwe likely won’t, absent testing.<\/p>\n<\/blockquote>\n

Jeremy W. Sherman<\/a>:<\/p>\n

\n

David’s concern is that,\n“It’s up to the programmer to realize that we have actually not created all of the proofs required to prove correctness.”\nThis concern arises from his thinking that the proof for\nnegb_inverse<\/code> goes through\neven if you alter negb<\/code> so it always returns true<\/code>.<\/p>\n

The version of negb<\/code> he defines that always returns true<\/code>\nactually already fails at the negb_inverse<\/code> theorem,\nwithout need to proceed to trying to prove negb_ineq<\/code>.<\/p>\n

[…]<\/p>\n

David’s core concern about knowing you’ve proved what you want to prove is a real problem.<\/p>\n<\/blockquote>","protected":false},"excerpt":{"rendered":"

Jeremy W. Sherman: A dependent type is a type that depends, not just on other types, but on terms. This means you can have values – plain old data – in your types. A common example is that of length-indexed lists. You likely caught on that that code is Swift-ish but not actually Swift. That’s […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"apple_news_api_created_at":"","apple_news_api_id":"","apple_news_api_modified_at":"","apple_news_api_revision":"","apple_news_api_share_url":"","apple_news_coverimage":0,"apple_news_coverimage_caption":"","apple_news_is_hidden":false,"apple_news_is_paid":false,"apple_news_is_preview":false,"apple_news_is_sponsored":false,"apple_news_maturity_rating":"","apple_news_metadata":"\"\"","apple_news_pullquote":"","apple_news_pullquote_position":"","apple_news_slug":"","apple_news_sections":"\"\"","apple_news_suppress_video_url":false,"apple_news_use_image_component":false,"footnotes":""},"categories":[4],"tags":[263,46,71,901],"class_list":["post-12168","post","type-post","status-publish","format-standard","hentry","category-programming-category","tag-theory","tag-languagedesign","tag-programming","tag-swift-programming-language"],"apple_news_notices":[],"_links":{"self":[{"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/posts\/12168","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/comments?post=12168"}],"version-history":[{"count":3,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/posts\/12168\/revisions"}],"predecessor-version":[{"id":12420,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/posts\/12168\/revisions\/12420"}],"wp:attachment":[{"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/media?parent=12168"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/categories?post=12168"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/tags?post=12168"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}