checked htdp comments in python using interactive unification

checked_comments_example.py

# thank you to matthias for providing this example.

def g(y : "number") -> "number":
    return y + 1

def f(x : "i dont know i think this param is dropped") -> "a function":
    return g

h : "scary function" = f(10)

a : "int" = h(22)



# the questions that the user is asked: (probably not in order)

# do the type comments "a function" and ("number", "number") refer to the same concept? Y

#  equivalence classes: [["a function", ("number", "number")]]

# do the type comments "scary function" and "a function" refer to the same concept? Y

#                       [["a function", ("number", "number"), "scary function"]]

# do the type comments "int" and "number" refer to the same concept? Y

#                       [["int", "number"], ["a function", ("number", "number"), "scary function"]]

idea.py

# hello matthias, this is an idea i've had.
# I've been programming a bunch in python for my coop, and it made me think of a couple things you said in UG PL lecture.
# most notably, that comments are communications to future programmers, and that types serve a similar purpose.

# now, when I write python code, I find writing the types as comments fundies 1 style to be extremely effective.


# consider this snippet from my job, converting a list of "nodes", and a root path into an "xmlnode".
# this example uses nothing special except the recommended comment style from __how to design programs__.


# SNIPPET START ------------------- {
from xml.etree.ElementTree import Element, SubElement, Comment, tostring

# [node] -> xmlstring -> xmlnode
def makemap(nodes, path):
    # take a list of nodes, and add them to root
    mm = Element("map")
    mm.set("version", "freeplane 1.8.10")
    mm.append(Comment("this is a generated freeplane file"))
    r = Element("root", {"a": nodes})
    mm.append(r)
    return Element("final", {"a": mm})


nodes = [("pretend this is a node", x) for x in map(str,range(10))]
path = "i want this string in my xml node"
makemap(nodes, path)

# SNIPPET END ------------------- }

# adding the type annotation comment in the style of how to design programs (htdp) provides a lot of the important funcitonality of type systems imo 
# fundies 1 students know this very well. The jump from fundies 1 (racket with type comments) to fundies 2 (java) in terms of type system
# assistance is insignificant. Java's type system mostly slows you down for small programs compared to racket (this claim is anecdotal but I beleive it)
# benefits of type comments :
#   * communication to future programmers including yourself
#   * help you break down the problem and keep track of your thinking (wish list) as you design the program.


# another fun thing type annotation comments do (when I do it at least), is that the "comment type" of something is not a definite
# thing, it's nebulous and it evolves as the program evolves. "xmlnode" and "xmlstring" are not types but descriptions



# maybe you will see where this is going. lets adapt the above snippet to use python type annotations: arbitary expressions that are ignored at runtime
# SNIPPET START ------------------- {

def makemap(nodes: "[nodes]", path: "xmlstring") -> "xmlnode":
    # ...
    # snip
    # ...
    return Element("final")


nodes : "[node]" = [("pretend this is a node", x) for x in map(str,range(10))]
path : "xmlstring" = "i want this string in my xml node"
makemap(nodes, path)

# SNIPPET END ------------------- }


# now it gets fun.
# there is an api to read this annotation data, so fun tools can be used to check properties on python files
# most notably the mypy, which adds a standard (as far as I can tell) type system to python.

# so here I propose a new tool : a python "opt-in type checker" like mypy but really its a "comment checker"
# "opt-in" means it will pass every single python program as is, It will only give an error if some of the users
# established constraints conflict by the users's own standards. It does not find errors, it helps the user check their own
# constraints.

# the core of a type checker is the equality algorithm, how it compares two types as equal (to find which ones aren't)

# so how do we write an algorithm to compare equality of two types which are arbitrary english sentences ? the answer is we don't.
# I argue that with user interaction we don't need to write an algorithm to do it, we can just make the user do it.

# three things: 1. if the users editor is set up for this, most types will be 100% perfect matches, because autocomplete groups similar strings into identical ones.
#
#               2. in nontrivial cases, the user can be asked each unification question interactively.
#                     a. in a cli tool or IDE, give the user this yes or no question: "Are type A and type B referring to the same concept? Y/N"
#
#                     b.     where A is one of = "apple",                    | "xmlnode thing thats supposed to eventually have .display method"| "integer"
#                              and B is one of = "red fruit"                 | "xmlnode"                                                        | "number of apples (but don't let it get super high!!)"
#
#                     c. assuming the user answers yes to all the questions above, the equivalence can be transitively extended to a more categories.
#                            where C is one of = "(color, ripeness, radius)" | "python class ElementTree"                                       | "number of apples"
#
#               3. this wouldn't scale immeditaely to nontrivial programs, so maybe there is some clever way to cache user
#                         created equivalence classes between runs, I don't know


# this would not give any of the safety guarentees of type systems but it would give many of the mental benefits
# of type systems : you don't have to keep track of what type of "thing" each variable is, and invariants you put down in types are communicated to other parts of the program.

# also consider how flexible it is: if you wanted to include nullability into the design of your program, just start throwing around questions marks

# this was born out of a frustration with (trying to) read uncommented python code for my job

my editor colors comment strings and expression strings differently (because of emacs-tree-sitter)

Also made this animation not because it was necessary but because animations are fun.