Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
429 lines (407 sloc) 13.6 KB
# The contents of this module are described in Stephen Dolan's thesis:
# "Algebraic Subtyping" (Sep 2016) https://www.cl.cam.ac.uk/~sd601/thesis.pdf
doc = path("doc:/subtyping")
# To avoid the adherence into a specific typing scheme, this
# system does not provide head constructors. The interface for
# head constructors should be passed in as a parameter:
# The 'is_subtype(x, y)' should give true/false
# if the x is subtype of y.
# Each head constructor must implement method 'merge_to(group, pol)'
# where group is a set, polarity is +1 or -1.
# The purpose of this function is to allow the head constructor
# to compact itself into a group.
# Simplest implementation of merge_to is to just do 'group.add(self)'
# If you attempt to do something more than that, it should not affect
# the outcome of the is_subtype -check in the biunify -method.
# The head constructor in a positive port would be likely best treated
# as a set of properties some value can satisfy, whereas the same
# constructor in a negative port would mean that those properties are
# required.
# The 'merge_to' must always succeed because it may be also used when
# printing the type. Prefer tainting the type, if you have to fail there.
# One flow pair per a variable
flow_pair = (neg = Port(-1), pos = Port(+1)):
neg.flow.add(pos)
pos.flow.add(neg)
return (neg = neg, pos = pos)
# The type inferencing information for one translation unit.
class TypeEngine
+init = (self, is_subtype):
self.visited = set()
self.is_subtype = is_subtype
# Verifies that something coming out from 'p' can go into 'q'
biunify = (self, p, q):
pq = [p, q]
return if pq in self.visited
self.visited.add(pq)
assert p.pol > q.pol, "biunify polarities must be (+p, -q)"
# Solves the t1 <= t2 constraints
for x in p.heads
for y in q.heads
assert self.is_subtype(x, y), "type flow constraint violation"
# Solves the t1 <= b
for s in q.flow
merge(s, p)
# Solves the a <= t2
for s in p.flow
merge(s, q)
# Solves the constraint decomposition
for label, s1 in p.transitions.items()
s2 = q.transitions.get(label, [])
if label.invert
for t1 in s1
for t2 in s2
self.biunify(t2, t1)
else
for t1 in s1
for t2 in s2
self.biunify(t1, t2)
# This makes it easy to match labels in the transition flow.
class LabelSet
+init = (self):
self.labels = {}
get = (self, group, invert=false):
label = self.labels.get(group)
if not label
self.labels[group] = label = (group=group, invert=invert)
else
assert label.invert == invert, "similar labels must maintain similar polarity rules"
return label
# The 'port' conveys the idea that something goes in or out. If it's
# a negative port, something goes in. If positive, something goes out.
class Port
+init = (self, pol=+1):
self.pol = pol
self.heads = set()
self.flow = set() # double-link
self.transitions = {}
add_transition = (self, label, port):
if label.invert
assert self.pol != port.pol, "polarity violation"
else
assert self.pol == port.pol, "polarity violation"
try
self.transitions[label].add(port)
except KeyError as _
self.transitions[label] = set([port])
+repr = (self):
a = []
for item in self.heads
a.append(repr(item))
return "{" ++ " ".join(a) ++ "}"
merge = (q1, q2):
assert q1.pol == q2.pol
for h in q2.heads
h.merge_to(q1.heads, q1.pol)
q1.flow.update(q2.flow)
for q3 in q2.flow
q3.flow.add(q1)
for label, s2 in q2.transitions.items()
try
q1.transitions[label].add(s2)
except KeyError as ke
q1.transitions[label] = set(s2)
# # Deciding subsumption allows giving type annotations for the programs. It
# # is given on the page 127
# subsume = (q1, q2, visited):
# assert q1.pol == q2.pol, "cases elided"
# if [q1, q2] in visited
# return true
# visited.add([q1, q2])
#
# for key in q1.terms
# t1 = q1.terms[key]
# t2 = q2.terms.get(key)
# if not t2
# return false
# if not t1.subsume(t2)
# return false
# for pair in t1.pairs(t2)
# if not subsume(pair[0], pair[1], visited)
# return false
# return true
#
# # "The simplest way to construct a type automaton from a positive or negative
# # type is to first construct a type automaton containing extra transitions labelled
# # by and then to remove these transitions in a second pass. This mirrors the
# # standard algorithm for constructing a nondeterministic finite automaton from
# # a regular expression"
# construct = (groups, c_pol=1):
# flow = {+1:{}, -1:{}}
# recs = {}
# visits = set()
# visit_pos = (g):
# return visit(g, +1, visit_pos, visit_neg)
# visit_neg = (g):
# return visit(g, -1, visit_neg, visit_pos)
# visit = (g, pol, posf, negf):
# assert g not in visits
# visits.add(g)
# if isinstance(g, VarRepr)
# if g in recs
# return recs[g]
# try
# return flow[pol][g]
# except KeyError as ke
# flow[pol][g] = qs = set([Type(pol)])
# return qs
# q = Type(pol)
# if isinstance(g, Group)
# assert g.pol == 0 or g.pol == pol
# if g.rec
# recs[g.rec] = q
# q.terms[null] = block = []
# for t in g.terms
# block.extend( visit(t, pol, posf, negf) )
# if g.rec
# recs.pop(g.rec)
# else
# term = g.construct(posf, negf)
# q.terms[interface(term)] = term
# return set([q])
# tmp = []
# for group in groups
# if c_pol < 0
# tmp.append(visit_neg(group))
# else
# tmp.append(visit_pos(group))
# # flow edge construction:
# # (q-) ----> (q+)
# # a in H(q-), a in H(q+)
# for var in flow[-1]
# bs = flow[+1].get(var, [])
# for a in flow[-1][var]
# for b in bs
# a.flow.add(b)
# b.flow.add(a)
# builder = DFABuilder()
# out = []
# for q in tmp
# out.append(builder.get(q, c_pol))
# builder.finalize()
# return out
#
# deconstruct = (nodes):
# builder = DFABuilder()
# dfa = []
# for node in nodes
# dfa.append(builder.get(set([node]), node.pol))
# builder.finalize()
#
# flow_edges = []
# vartab = {}
# for node in builder.postorder
# vartab[node] = set()
# if node.pol < 0
# for other in list(node.flow)
# flow_edges.append([node, other])
# node.flow.clear()
# for edge in flow_edges
# admissable(edge[0], edge[1])
#
# vars = blank_labels()
# while true
# best = 0
# biclique = null
# for node in builder.postorder
# a = set(node.flow)
# b = set()
# count = 0
# for x in a
# for y in x.flow
# if y not in b and y.flow >= a
# b.add(y)
# count += 1
#
# if count > best
# biclique = [a, b]
# best = count
# if best == 0
# break
# var = VarRepr(vars.next())
# a = biclique[0]
# b = biclique[1]
# for x in a
# x.flow.difference_update(b)
# vartab[x].add(var)
# for x in b
# x.flow.difference_update(a)
# vartab[x].add(var)
#
# recurs = {}
# lateral = {}
# decon_pos = (n):
# return decon(n, +1, decon_pos, decon_neg)
# decon_neg = (n):
# return decon(n, -1, decon_neg, decon_pos)
# decon = (ns, pol, posf, negf):
# if ns in recurs
# recg = recurs[ns]
# if not recg.rec
# recg.rec = VarRepr()
# return Group([recg.rec], pol)
# recurs[ns] = group = Group([], pol)
# for n in ns
# assert n.pol == pol
# for term in n.terms.values()
# group.terms.append(term.deconstruct(posf, negf))
# group.terms.extend(vartab[n])
# #group.terms.sort((a, b):
# # a.order > b.order)
# if group.terms.length == 0
# if ns in lateral
# other = lateral[ns]
# if other.terms.length == 0
# other.terms.append(VarRepr(vars.next()))
# group.terms.extend(other.terms)
# else
# lateral[ns] = group
# recurs.pop(ns)
# return group
#
# out = []
# for n in dfa
# if n.pol > 0
# out.append(decon_pos(set([n])))
# else
# out.append(decon_neg(set([n])))
# return out
#
# # flow edge simplification:
# # A flow edge q- ----> q+ is admissable iff t- <= t+
# # where the types t-, t+ are the types represented by q-, q+
#
# # "This suggests a straightforward heuristic algorithm for optimising the set
# # of flow edges in a scheme automaton. First, we remove all of them. Then, we
# # add them back one at a time, skipping any that are admissable. While the
# # success of this heuristic depends greatly on the order flow edges are processed
# # in, I found that a reverse postorder traversal (so that flow edges on child nodes
# # are processed before parents) gave good results."
#
# # "Of course, in order to implement this we must have an algorithm that
# # decides subtyping problems of the form t- <= t+ (recall that biunification
# # operates on constraints t+ <= t-, so it is unsuitable). Such an algorithm
# # is described in Chapter 8, as it forms the core of the subsumption algorithm."
# admissable = (q1, q2):
# if q2 in q1.flow
# return true
# else
# q1.flow.add(q2)
# q2.flow.add(q1)
# if q1.terms.length == 0
# return true
# for key in q1.terms
# t1 = q1.terms[key]
# t2 = q2.terms.get(key)
# if not t2 # These two might mean for worse problems.
# return true
# if not t1.subsume(t2)
# return true
# res = false
# for pair in t1.pairs(t2)
# res |= admissable(pair[0], pair[1])
# if res
# return true
# q1.flow.discard(q2)
# q2.flow.discard(q1)
# return false
#
# class DFABuilder
# +init = (self):
# self.assoc = {}
# self.visited = {}
# self.postorder = []
#
# get = (self, nodeset, pol=+1):
# if pol >= 0
# return self.build(nodeset, +1, self.pos, self.neg)
# else
# return self.build(nodeset, -1, self.neg, self.pos)
#
# pos = (self, nodeset):
# return set([self.build(nodeset, +1, self.pos, self.neg)])
#
# neg = (self, nodeset):
# return set([self.build(nodeset, -1, self.neg, self.pos)])
#
# build = (self, nodeset, pol, posf, negf):
# for n in nodeset
# nodeset.update(n.terms.get(null, []))
# node = self.visited.get(nodeset)
# if node
# assert node.pol == pol, "polarity conflict"
# return node
# self.visited[nodeset] = node = Type(pol)
# for n in nodeset
# assert n.pol == pol, [n.pol, pol]
# for type in n.terms
# if type == null
# continue
# term = n.terms[type].construct(posf, negf)
# dst = node.terms.get(type)
# if dst
# dst.merge(term, node.pol)
# else
# node.terms[type] = term
# try
# self.assoc[n].add(node)
# except KeyError as ke
# self.assoc[n] = set([node])
# for key in node.terms
# node.terms[key] = node.terms[key].construct(posf, negf)
# self.postorder.append(node)
# return node
#
# finalize = (self):
# for edge in self.visited.items()
# node = edge[1]
# for n in edge[0]
# for f in n.flow
# node.flow.update(self.assoc.get(f, []))
# node.flow.discard(node)
#
# # TODO: treat printing as a separate problem?
# blank_labels = ():
# a = ord('a')
# i = 0
# while true
# lab = chr(a + i % 26)
# n = i // 26
# while n > 0
# lab = chr(a + n % 26) ++ lab
# n = n // 26
#
# yield lab
# i += 1
#
# class VarRepr
# +init = (self, name=null):
# self.name = name
#
# +repr = (self):
# if self.name
# return self.name
# else
# return "<var>"
#
# class Group
# +init = (self, terms=[], pol=0):
# self.pol = pol
# self.terms = terms
# self.rec = null
#
# +repr = (self):
# assert not self.rec
# "implement recursion repr"
# res = []
# for i in self.terms
# res.append(repr(i))
# if res.length == 0
# if self.pol > 0
# return "(bot)"
# else
# return "(top)"
# if self.pol > 0
# return "(" ++ " | ".join(res) ++ ")"
# else
# return "(" ++ " & ".join(res) ++ ")"