Named Parameters

There’s a pretty interesting proposal discussion on swift-evolution right now: Naming Functions with Argument Labels.

I bring it up because it hits a bit close to my heart with regards to naming of functions named arguments. It’s my opinion that Swift should have diverged from ObjC here and treated named arguments properly. What I mean by that is to move the argument name within the function parameters completely.

So a function name like this:

func insertSubview(view, aboveSubview) {}

Would have become:

func insert(subview, aboveSubview)

The difference is the lack of the implicit _ on the first argument name. I bring this up (again) because of the given proposal shows well why I think the current convention stinks.

let fn = someView.insertSubview(_:aboveSubview:)

Ick! Why is that _ necessary. Oh‚Ķ right, because we’ve shoved the actual parameter name for that first item into the name of the function. ObjC did this for a compelling reason. Swift seems to simply follow that convention for what I can only presume to be convenience in the Swift to ObjC interop.

Too bad, this seems so much nicer to me:

let fn = someView.insert(subview:aboveView:)

Maybe someday…

Named Parameters

RE: Why Swift guard Should be Avoided

I saw this blog article, Why Swift guard Should Be Avoided, and it got me thinking about things I believe are fallacies but are continued to be talked about as the “right way to program”. I will preface this by saying that I don’t think there is a “right way” to program, but rather, there are trade-offs for particular paths that we chose to go down. Some of these paths provide better fruit than others. However, just as fruits have seasonality to them, some paths might not always produce the best fruit in all circumstances. Context matters. All that said, I still believe that are paths that never produce good fruit, and I think two of those paths are demonstrated in the linked blog article.

So, what are these bad paths (or as I call programming fallacies)?

  1. Functions should be between 6 and 10 lines 2. Single Responsibility means doing only one thing

The first is an arbitrary way to determine quality and complexity of code that holds no bearing in the actual domain of the problem. It also asserts that shorter code is better than longer code with no real presumption on the complexity of the shorter code. I believe that code clarity is far more important than code length.

The quote presented to defend this was from Robert C. Martin:

The first rule of functions is that they should be small. The second rule of functions is that they should be smaller than that.

Here’s what I believe is a better philosophical position:

Functions should be as small as possible to do there job, but no smaller than that.

The other fallacy is that “single responsibility” means a single action. This leads you down the path of premature refactoring, which I’ll talk about a bit with examples from the post. A function should do a single task, but tasks are generally multi-step transactions. This should be completely obvious because we still need to have the vend() function; without it, we have to duplicate the logic everywhere in which a vend() must take place.

Pre-mature Refactoring

Ok, let’s get into the post a bit. Here’s the Swift code from Apple’s example:

struct Item {
    var price: Int
    var count: Int
}

enum VendingMachineError: ErrorType {
    case InvalidSelection
    case InsufficientFunds(coinsNeeded: Int)
    case OutOfStock
}

class VendingMachine {
    var inventory = [
        "Candy Bar": Item(price: 12, count: 7),
        "Chips": Item(price: 10, count: 4),
        "Pretzels": Item(price: 7, count: 11)
    ]

    var coinsDeposited = 0

    func dispense(snack: String) {
        print("Dispensing \(snack)")
    }

    func vend(itemNamed name: String) throws {
        guard var item = inventory[name] else {
            throw VendingMachineError.InvalidSelection
        }

        guard item.count > 0 else {
            throw VendingMachineError.OutOfStock
        }

        guard item.price <= coinsDeposited else {
            throw VendingMachineError.InsufficientFunds(coinsNeeded: item.price - coinsDeposited)
        }

        coinsDeposited -= item.price
        --item.count
        inventory[name] = item
        dispense(name)
    }
}

And here’s the refactored version from the post:

func vend(itemNamed name: String) throws {
    let item = try validatedItemNamed(name)
    reduceDepositedCoinsBy(item.price)
    removeFromInventory(item, name: name)
    dispense(name)
}

private func validatedItemNamed(name: String) throws -> Item {
    let item = try itemNamed(name)
    try validate(item)
    return item
}

private func reduceDepositedCoinsBy(price: Int) {
    coinsDeposited -= price
}

private func removeFromInventory(var item: Item, name: String) {
    --item.count
    inventory[name] = item
}

private func itemNamed(name: String) throws -> Item {
    if let item = inventory[name] {
        return item
    } else {
        throw VendingMachineError.InvalidSelection
    }
}

private func validate(item: Item) throws {
    try validateCount(item.count)
    try validatePrice(item.price)
}

private func validateCount(count: Int) throws {
    if count == 0 {
        throw VendingMachineError.OutOfStock
    }
}

private func validatePrice(price: Int) throws {
    if coinsDeposited < price {
        throw VendingMachineError.InsufficientFunds(coinsNeeded: price - coinsDeposited)
    }
}

Let’s break it down:

vend(itemNamed name: String) throws

The author suggests that the refactored version is better. But here’s the first thing to note: the responsibility of the function has not changed; it is still responsible for doing the same thing it did before. So in the first regard, nothing should have changed from an API usage standpoint. This is vital because when we refactor functionality, this is the actual goal: to break about couple functionality that didn’t belong together.

private func validatedItemNamed(name: String) throws -> Item

I actually don’t know what this is supposed to do. In order to follow what is going on, I need to actually read through the code all of the code that it calls. Doing that, I can see that it does the following:

  1. Ensures the item is in the dictionary 2. That the count of items is not zero 3. That the number of coins deposited is greater than or equal to the price of the item

However, this took four functions and three levels of function calls to achieve. The oversight in this approach is that it is inherently fragile because it makes use of four functions to achieve it’s goal. A change to any single function can have a ripple effect on unintended side-effects.

Example: The vending machine needs a new function, addItem(). It’s purpose is to allow additional items to be added to the vending machine. However, there are some constraints we want to add for new items:

  1. The name must not be empty 2. The name must be word-capitalized (e.g. Big Candy Bar) 3. The price must be less than 100

I can pretty much guarantee you that the validateItem() function is going to be updated here to add these requirements. So not only are we going to be validating things that we simply don’t care about on ever call to vend(), if there is a data already in the vending machine that doesn’t already meet these requirements, the vend() is going to fail.

This may seem like a contrived example, but it absolutely is not. I’ve had to fix issues like this in real code because of this exact type of refactoring.

reduceDepositedCoinsBy(price: Int)

This function will lead to data corruption. It makes the assumption that validate() has been called. This function, if we’re going to actually have it, should actually do the verification that this is a legal operation. Otherwise, there is absolutely no purpose for it.

removeFromInventory(var item: Item, name: String)

Same comments apply here as well: data corruption!

itemNamed(name: String) throws -> Item

This one is an interesting one. If Swift had throwable subscripts, then this wouldn’t be necessary. However, I think in principle, this one is good, but the implementation is prone to bugs. This is the poster child for the guard statement.

private func itemNamed(name: String) throws -> Item {
    guard let item = inventory[name] {
        throw VendingMachineError.InvalidSelection
    }
    return item
}

This is objectively better as it ensures that the only code-path that can exist after the guard is one where the dictionary actually has the item. If also ensures that if the dictionary doesn’t have the item, we error out early.

Summary

Be wary of refactoring to meet arbitrary goals. When that is the purpose of the refactoring, it is very easy to get into a spot that you’ve actually created more complexity and introduced more error paths in your code.

My guiding principle: a function should handle it’s responsibility and only its responsibility. The number of steps for that responsibility is mostly immaterial.

RE: Why Swift guard Should be Avoided

Efficient Mutation

Here's the thing – I'm not very good at the whole concept of dealing with non-mutating data. Partly because I have a super difficult time understanding how you can write programs as the primary function of a program is to mutate data. So it's hard for me to grok the reason for design decisions such as "no pointers" and type-defined value/reference semantics. To me, they are actually a detriment to understanding how a program works.

So, I thought I'd post this to see if I can get some help from the community. I'll be glad to be corrected on this issue as I genuinely do not understand why there is this huge strive for immutable data everywhere.

Disclaimer: I completely understand why portions of your code would use immutable data; protecting yourself or others from accidentally causing side-effects is usually a good thing. That's not what I'm asking about though.

Ok, so what's the problem? That's easy: a syntax tree. I always find it best to ground my examples in real-world examples, and as I'm working on a programming language (Proteus) in my spare time, this seems like a great candidate.

The question is: how can I build up a tree over time efficiently without mutating but by retrieving new copies of the data? Further, how can I modify just a portion of the tree without needing to perform a copy of the entire tree?

It's the latter question that I'm really more interested in. I can completely see how the compiler could optimize away the copy while a type is being additively modified, especially since there are no other references to it. However, let's say you're building a code editor and you change the name of a function. There's no reason to re-parse the entire file; you know the location of the function in the file and where it sits in the AST, so the parse should be able to just parse the surrounding change and apply the delta to the tree.

Another way that I think about this problem is through the lens of a stream of changes that happen to the tree over time. So let's say we have the following stream:

  1. Parse top-level node (delta: add root node)
  2. Parse func decl (delta: add child to root node)
  3. Parse func body (delta: add children to func decl node)

Right, these are some very high-level deltas. With these three deltas, I don't see how to avoid the copy in the non-mutable world of the top-level node multiple times. In the world of mutation, I'd simply append the child to the parent for each of these deltas.

Am I just misunderstanding something?

To me, the efficiency of the program is extremely important. That's the time that the user is going to spend waiting for your code to run; it's important.

Efficient Mutation

Swift and Visual Studio Code

If you've been living under a rock, you might not know that Microsoft released a new editor (focused on web development): Visual Studio Code.

So… is it really just for web development? Honestly, it doesn't matter if it starts out that way because the thing that Microsoft tends to always get right is extensibility. We'll be able to start building plug-ins as the product matures to enable all sorts of development, including Swift!

Syntax Highlighting

Ok, the first thing that we need are the nice colors! This is actually fairly trivial to do:

  1. Open up the package contents of the Visual Studio Code app 2. Navigate to Contents/Resources/app/plugins 3. Create a new folder: vs.languages.swift 4. Place these three files into the created folder:
    1. swiftDef.js
    2. swiftMain.js
    3. ticino.plugin.json 5. Restart Visual Studio Code and open a Swift file!

You should see something like this:

Swift with basic syntax highlighting.

Note that this is just the most basic of highlighting that supports basic comments, strings, and keywords. More to come later!

Building

Next up, build errors! Again, this is also quite trivial to setup. You'll need to create a new build task. You can do this in a couple of ways. The easiest is:

  1. ‚åòP to bring up the command palette 2. Type build and press RETURN 3. There will be a prompt that you have not tasks; create the task 4. This will create a .settings folder with a tasks.json file

The contents of the file should be:

{
    "version": "0.1.0",
    "command": "swiftc",
    "showOutput": "silent",

    "args": ["main.swift"],

    "problemMatcher": {
        "pattern": {
            "regexp": "^(.*):(\\d+):(\\d+):\\s+(warning|error):\\s+(.*)$",
            "file": 1,
            "line": 2,
            "column": 3,
            "severity": 4,
            "message": 5
        }
    }
}

Now, you can press ‚áß‚åòB now to build. If you have an error, press ‚áß‚åòM to show the error pane.

Swift with a build error shown.

Next Steps

I'll probably be taking a look at making the editing experience better by playing around with the options for syntax highlighting. I also want to take a look at building a language service, though, officially this is not yet supported.

Goodie Bin

Ok… if you want to contribute to this, I've actually posted a fill GitHub repo here: https://github.com/owensd/vscode-swift.

What I actually have done, instead of creating a directory, is create a link within the Visual Studio Code package to my repo location on disk.

  1. cd /Applications/Visual\ Studio\ Code.app/Contents/Resources/app/plugins 2. ln -s <path/to/repo> vs.languages.swift 3. Restart Visual Studio Code

Voilà!

Swift and Visual Studio Code

Switch Statement Matching

What is the output of this problem?

let x = 5, y = 10

switch (x, y) {
case (_, _):
    println("_, _")

case (5, _):
    println("5, _")

case (_, 10):
    println("_, 10")

case (5, 10):
    println("5, 10")
}

If you said, "", then great! If you're sad that case (5, 10): doesn't match… well, you're not alone.

Friendly reminder, always read your swift-statements like a chain of if-statements. With pattern matching in Swift, this could be the source of some inadvertent bugs, especially when adding new case clauses.

UPDATE: I filed rdar://21001503 about having a warning for case statements that can not be reached.

Switch Statement Matching

Brent’s Week 3 Bike Sheed

If you're not following Brent Simmons, then go here first: http://inessential.com/langvalue.

Ok, now that you've read that, you should probably stop reading here until you go and try to solve the problems there. For extra points, only pick one of the struct/enum choices and pick one of the protocol based choices.

I'll wait…


If you've been following along with any of Brent's posts, you might notice that he has (intentionally?) created a problem that will help you uncover some of the limitations of Swift's type system based on some of his own frustrations (see his KVC diary posts). Nonetheless, it is good to compare what options are on the table when a problem like he presented is put before us.

Now, if you've only played with Swift on the surface, you might not know the gotcha's yet. Also, you've probably heard a bit about "PROTOCOLS, PROTOCOLS, PROTOCOLS!". Naturally, you might say to yourself, "AHA! The protocol solution must be the 'right one', 'best one', or the 'easiest one' to implement."

However, if you have been around Swift for a while, I'm sure you noticed that Brent has fiendishly put a requirement of Set<T>.

Meme - Train on bridge falling off, Caption: Use Protocols They Said... It's Awesome They Said...

So there's a dirty little (apparent) problem with protocols today… once they get a Self requirement, hetergenous usage of them goes out the window for any strongly typed collection.

But… maybe this is a sign. Maybe the "protocols first" approach tells us something. After all, implementing the protocol version of Brent's question is actually not even supported today in Swift (option 4 at least).

Solving the Problem

Let me suggest something: the spec artificially makes the problem harder and implies that protocols should be used in a way that I do not think Swift intends you to use them. Protocols are not types, they do not behave like types, and they cannot be used like types.

I think the better option to solving the problem presented is option #5: using enums and protocols.

Enums

The problem statement is very clear: there are three, and only three, different type constructs that are allowed. Namely:

  • Integer
  • String
  • Table

To me, this clearly implies that an enum is going to be the right structure to use.

enum LangValue {
    case IntegerValue(Int)
    case StringValue(String)
    indirect case TableValue([String:LangValue])
}

Beautiful. Seriously, I think that is an extremely clear and precise model of exactly what we want.

Now, we need to add a type function. So the complete, initial model looks like this:

enum LangValueType {
    case Integer
    case String
    case Table
}

enum LangValue {
    case IntegerValue(Int)
    case StringValue(String)
    indirect case TableValue([String:LangValue])

    var type: LangValueType {
        switch self {
        case .IntegerValue(_): return .Integer
        case .StringValue(_): return .String
        case .TableValue(_): return .Table
        }
    }
}

Protocols

OK, now here is where I think protocols should be used. You see, the spec now asks for four different classes of behaviors:

  • Convertible to an Integer
  • Convertible to a String
  • Addable
  • Storable (my term for the dictionary-like operations)

To me, this screams protocols.

protocol IntegerConvertible {
    func integerValue() throws -> Int
}

protocol StringConvertible {
    func stringValue() throws -> String
}

protocol Addable {
    typealias AddableType
    func add(other: AddableType) throws -> AddableType
}

protocol Storeable {
    typealias ValueType
    typealias KeyType

    mutating func set(object object: ValueType, forKey key: KeyType) throws
    mutating func remove(forKey key: KeyType) throws
    func object(forKey key: KeyType) throws -> ValueType?
    func keys() throws -> [KeyType]
}

Notice something: none of these protocols are tied to the LangValue type. If a type is needed, a typealias is used to make this generic so that these protocols can be applied to any type. This is key (and goes a bit against some of my previous recommendations about not making protocols generic).

Now it's simply a matter of applying these protocols to our type:

extension LangValue : IntegerConvertible {
    func integerValue() throws -> Int {
        switch self {
        case let IntegerValue(value): return value
        case let StringValue(value): return (value as NSString).integerValue
        default: throw LangCoercionError.InvalidInteger
        }
    }
}

extension LangValue : StringConvertible {
    func stringValue() throws -> String {
        switch self {
        case let IntegerValue(value): return NSString(format: "%d", value) as String
        case let StringValue(value): return value
        default: throw LangCoercionError.InvalidString
        }
    }
}

extension LangValue : Addable {
    func add(other: LangValue) throws -> LangValue {
        switch (self, other) {
        case let (.IntegerValue(lvalue), .IntegerValue(rvalue)):
            return .IntegerValue(lvalue + rvalue)

        case (.StringValue(_), .IntegerValue(_)): fallthrough
        case (.IntegerValue(_), .StringValue(_)): fallthrough
        case (.StringValue(_), .StringValue(_)):
            return try LangValue.StringValue(self.stringValue() + other.stringValue())

        default: throw LangCoercionError.InvalidAddition
        }
    }
}

extension LangValue : Storeable {
    mutating func set(object object: LangValue, forKey key: String) throws {
        switch self {
        case let .TableValue(table):
            var copy = table
            copy[key] = object
            self = LangValue.TableValue(copy)

        default: LangCoercionError.NotOfTypeTable
        }
    }

    mutating func remove(forKey key: String) throws {
        switch self {
        case let .TableValue(table):
            var copy = table
            copy.removeValueForKey(key)
            self = LangValue.TableValue(copy)

        default: throw LangCoercionError.NotOfTypeTable
        }
    }

    func object(forKey key: String) throws -> LangValue? {
        switch self {
        case var .TableValue(table):
            return table[key]

        default: throw LangCoercionError.NotOfTypeTable
        }
    }

    func keys() throws -> [String] {
        switch self {
        case let .TableValue(table):
            return Array(table.keys)

        default: throw LangCoercionError.NotOfTypeTable
        }
    }
}

Conclusion

So that's it, that's the basic approach to the problem that I think is a concise, clear model of the specification. It doesn't exactly fit the asks from the four options, but I think it is the better approach.

Full source code here: https://gist.github.com/owensd/33d85872c15c2b496515

Brent’s Week 3 Bike Sheed

Beware of the Enum

So apparently enums are still a flaking beast (Xcode 7.0 GM).

enum Awesome {
    case HowAwesome(String)
    case KindaAwesome
    case NotReallyAwesome
}

let a = Awesome.HowAwesome("THIS AWESOME")
let b = Awesome.KindaAwesome
let c = Awesome.NotReallyAwesome

print(a)
print(b)
print(c)

Ok, this code seems fine, and the output is:

HowAwesome("THIS AWESOME")
KindaAwesome
NotReallyAwesome

Now, let's image a new case statement is desired…

enum Awesome {
    case HowAwesome(String)
    case KindaAwesome
    case NotReallyAwesome
    case WithOutMeYouWouldBeHappy(String)
}

let a = Awesome.HowAwesome("THIS AWESOME")
let b = Awesome.KindaAwesome
let c = Awesome.NotReallyAwesome

print(a)
print(b)
print(c)

Here's the output:

HowAwesome("THIS AWESOME")
KindaAwesome
KindaAwesome

Yeah, not really that awesome. rdar://22915709.

Here's the clip from last night: https://youtu.be/DA-wjc6hwME?t=51m30s

UPDATE: 9:30am PDT, Sept 30, 2015

//platform.twitter.com/widgets.js

So yay! Maybe I should just switch to the beta…

Beware of the Enum

Associated Enum Cases as Types

This is a bit of a follow-up from my Enums with Associated Data vs. Structs. If you haven’t seen that, some of this might be a little out-of-context.

Another issue I run into with working with enums with associated data is actually getting the data out of them! Let’s take a look at the following code sample:

enum Token  {
    case Keyword(keyword: String, offset: Int)
    case Identifier(identifier: String, offset: Int)
}

//
// The declarations; no real issues here.
//

let importkey = Token.Keyword(keyword: "import", offset: 0)
let funckey = Token.Keyword(keyword: "func", offset: 0)

//
// The ways to match on a value and get some data out. Ugh!
//

if case Token.Keyword("import", _) = importkey {
    print("import keyword")
}

if case let Token.Keyword(keyword, _) = importkey {
    if keyword == "import" { print("import keyword") }
    if keyword == "func" { print("func keyword") }
}

switch importkey {
case let .Keyword(keyword): print("\(keyword) keyword")
case let .Identifier(identifier): print("\(identifier)")
}

All of those suck, in my opinion. There are a few of problems:

  1. If I want to store the result, I end up with a really stupid construct.
  2. If there are multiple associated data fields, I get lots of _ in the matches.
  3. They use this = somevar syntax that is completely unlike anything else in Swift.

What I wish had happened was to treat the case values as types. I’ve modelled what that would look like here:

enum Token  {
    case Keyword(keyword: String, offset: Int)
    case Identifier(identifier: String, offset: Int)

    var Keyword_ : (keyword: String, offset: Int)? {
        if case let .Keyword(keyword, offset) = self {
            return (keyword, offset)
        }
        return nil
    }

    var Identifier_ : (identifier: String, offset: Int)? {
        if case let .Identifier(identifier, offset) = self {
            return (identifier, offset)
        }
        return nil
    }
}

Imagine that Keyword_ and Identifier_ were implicitly created by the compiler. The idea is to make use of the other constructs of the language, in this case, Optional to allow us to access the inner details of the enum.

// It's a tuple, so access by index is allowed.
if importkey.Keyword_?.0 == "import" {
    print("import keyword")
}

// These are named tuples, so access by name is allowed.
if importkey.Keyword_?.keyword == "import" {
    print("import keyword")
}

if let keyword = importkey.Keyword_?.keyword {
    print("\(keyword) keyword")
}

Now, here’s the part I really don’t understand. Swift is already essentially doing this, we just don’t have access to it in any way other than the case pattern matching stuff. I think it would have been more preferable to do this:

if case ("import", _) = importkey.Keyword {
    print("import keyword")
}

To me, this makes it clear that tuples are all matched the exact same way. Instead, we have associated data in enums (which is essentially a tuple) matched one way, and tuples, that may have the exact same structure, matched a completely differently way.

rdar://22704262

Associated Enum Cases as Types

Enums with Associated Data vs. Structs

Maybe everyone can help me out here: I'm trying to find out what the value of enums with associated values is over structs that conform to a protocol.

Here's the context: I'm playing around with the parser code and I'm using an enum to describe what statements might look like in Proteus.

Let's say it looks like this:

enum Statement {
    case Import(keyword: Token, packageName: Token)
    case Assignment(binding: Token, value: Expression)
} 

Ok, so here's the issue. When I'm writing the parser, I want to have a function parseImport() to handle the actual parsing of the import construct. However, Swift doesn't allow me to define the function definition that I actually want:

func parseImport() throws -> Statement.Import { ... }

The thing is, I don't want parseImport to return any of the possible values for Statement; I only want the function to be able to return the specific case of Import. Furthermore, the data stored within each of the associated values isn't related.

So the question is, when is an associated value enum a better choice than structs? You see, I could define the above this way too:

protocol Statement {}

struct Import : Statement {
    let keyword: Token
    let packageName: Token
}

struct Assignment : Statement {
    let binding: Token
    let value: Expression
}

func parseImport() throws -> Import { ... }

The only clear win I see is that the enum version is more terse. At the end of the day, the usage code is pretty similar in the fact that each needs to determine what specific type of Statement is being dealt with, except I can remove the switch necessary to unpack the Statement.Import version.

There has to be some benefit right? Right now, I'm only see a downside, especially given the fact that I cannot model the desire to have a function return only a specific type of enum value.

UPDATE Sunday, September 13th, 2015 @ 11:49 PM PDT

I should have been a little less cavalier about the "some benefit". I understand that enums limit the potential values while protocols and structs allow this to be unbound. That's not really the problem though. The problem is about the coupling of the parts that make up the associated value of the enum with the notion of the actual type itself.

One suggestion to my dilemma was to essentially do the following:

typealias ImportStatement = (keyword: Token, packageName: Token)
typealias AssignmentStatement = (binding: Token, value: Expression)

enum Statement {
    case Import(ImportStatement)
    case Assignment(AssignmentStatement)
}

This allows the parseImport to return an ImportStatement instead. Of course, I then need to turn that into a Statement in my calling code. That kinda works; though it's much more tedious to actually do that, and it puts the construction of the actual type in the wrong location. Another problem with that approach is the assumption that I own the code. What if I was using a library that provided the enum, such as the one in Apple's Swift documentation:

enum Barcode {
    case UPCA(Int, Int, Int, Int)
    case QRCode(String)
}

Let's say I'm writing a parser for that and I want to write the parseUPCA function. What is the return type? Do I provide the loosely-typed version of parseUPCA() -> (Int, Int, Int, Int) and then have to pust the creation of the Barcode.UPCA instance at the caller (and if the UPCA data changes, it's more than a usage code update, I need to update all places that used the parts too, which is a potentially much more difficult search-and-replace fix)? Or return a Barcode and hope that I only ever get the UPCA version out of it?

I guess I just don't find any of the options available to us particularly good. In my code, Barcode.UPCA is all together a different type than Barcode.QRCode; I'd simply like to be able to actually model that.

So I need to ask myself: allow for the proper modelling of the type signatures or allow for the proper modelling of the closed nature of the types; I don't know how to do both in Swift today.

Enums with Associated Data vs. Structs

Dependent Types: I”m Missing Something

I’ve been seeing a bunch of mentions about dependent types on Twitter lately and saw this blog post get mentioned.

Clearly I’m missing something.

The goal is provably correct code. Ok, I’ll suspend the fact that in the real-world computer hardware actually fails or memory can be corrupted, and I’ll focus on the provability of the code being provably correct in the abstract sense.

I still don’t get it.

One of the article’s example is this:

func compare(x: UInt, y: UInt) -> NSComparisonResult {
    // BACKWARDS! IT LIES!
    // (And how many times have you accidentally flipped these?)
    return (x <= y) ? .OrderedDescending : .OrderedAscending
}

func compare(x: UInt, y: UInt) -> UInt {
    // I hope you weren't actually planning on relying on this function.
    return .OrderedAscending
}

Ok… let’s continue on.

Dependent types are provided to fix this:

enum Order(left: UInt, right: UInt) -> Type {
    /// Represents that `(left <= right)`.
    /// Witnessed by a proof that `left <= right`.
    case lessThanOrEqual(because: LEQ(x: left, y: right)):
        Order(left, right)

    /// Represents that `(left >= right)`.
    /// Witnessed by a proof that `right <= left`.
    case greaterThanOrEqual(because: LEQ(x: right, y: left)):
        Order(left, right)
}

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 dependently-typed code? Why? What’s preventing me from swapping left and right in the Order type that is returned?

I need to go and author more proofs to validate that the dependent types are all indeed correct.

Joe Groff tweeted this for some potential clarification:

//platform.twitter.com/widgets.js
In that link, we can see this example:

Definition negb (b : bool) : bool :=
match b with
    | true => false
    | false => true
end.

Definition negb' (b : bool) : bool :=
if b then false else true.

Theorem negb_inverse : forall b : bool, negb (negb b) = b.
destruct b.

But here’s the problem, this code also satisfies the proofs given so far:

Definition negb (b : bool) : bool :=
match b with
    | true => true
    | false => true
end.

Definition negb' (b : bool) : bool :=
if b then true else true.

Theorem negb_inverse : forall b : bool, negb (negb b) = b.
destruct b.

It’s up to the programmer to realize that we have actually not created all of the proofs required to prove correctness. So here’s my fundamental question: how do we know that we have enough proofs to actually prove our code is correct? I’ve only briefly looked over the topic, so maybe I’m simply missing the answer to this.

The paper does provide that last proof that we need:

Theorem negb_ineq : forall b : bool, negb b <> b.
destruct b; discriminate.
Qed.

But again, my question is how can we prove that we indeed have all of the proofs we need? Without that proof, I simply do not understand how dependent-types can actually produce provably correct code.

It’s an interesting topic; I’m not arguing against that or it’s application in domain spaces. I’m just trying to grok how this is objectively better than non-dependent-typed code with good test coverage. From a complexity standpoint, to me, it looks like a big loss; I get others will have less trouble on that end.

Dependent Types: I”m Missing Something