tommy-mor · March 25, 2021 19:14 · tommy-mor · Mar 22, 2021 · tommy-mor · Mar 23, 2021
diff --git a/checked_comments_example.py b/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"]]
diff --git a/idea.py b/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
	# 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"]]
	# 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