Class: Typisch::Type

Inherits:
Object
  • Object
show all
Defined in:
lib/typisch/type.rb,
lib/typisch/tuple.rb,
lib/typisch/object.rb,
lib/typisch/sequence.rb,
lib/typisch/subtyping.rb,
lib/typisch/type_checking.rb

Overview

Base class for types, with some convenience methods.

Note: since most of the algorithms on types (subtyping, union, intersection, …) operate on pairs of types, we don’t use methods on the actual type subclasses very much, since polymorphic dispatch on just one of the pair of types isn’t much use in terms of extensibility.

Instead the actual Type classes themselves are kept fairly lightweight, with the algorithms implemented separately in class methods.

Direct Known Subclasses

Constructor, NamedPlaceholder, Union

Defined Under Namespace

Classes: Any, Boolean, Constructor, Date, NamedPlaceholder, Nothing, Null, Numeric, Object, Sequence, String, Time, Tuple, Union

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Instance Attribute Details

#name ⇒ Object

Returns the value of attribute name.



68
69
70
 
# File 'lib/typisch/type.rb', line 68

def name
  @name
end

Class Method Details

.subtype?(x, y, may_assume_proven = {}, depth = 0) ⇒ Boolean

The core of the subtyping algorithm, which copes with equi-recursive types.

Actually quite simple on the face of it – or at least, short.

The crucial thing is that we allow a goal to be assumed without proof during the proving of its subgoals. Since (because of the potentially recursive nature of types) those subgoals may refer to types from the parent goal, we could otherwise run into infinite loops.

How’s that justified from a logic perspective? well, what we’re doing is, we’re just checking that the given subtyping judgement *isn’t* provably false under the inference rules at hand. This allows a maximal consistent set of subtyping judgements to be made.

Its dual, requiring that the judgement is provably true under the inference rules, would only allow a minimal set to be proven, and could get stuck searching forever for a proof of those judgements which are neither provably false nor provably true (namely, the awkward recursive ones).

See Pierce on equi-recursive types and subtyping for the theory: www.cis.upenn.edu/~bcpierce/tapl/, it’s an application of en.wikipedia.org/wiki/Knaster–Tarski_theorem to show that this is a least fixed point with respect to the adding of extra inferences to a set of subtyping judgements, if you note that those inference rules are monotonic. ‘Corecursion’ / ‘coinduction’ are also terms for what’s going on here.

TODO: for best performance, should we be going depth-first or breadth-first here?

Also TODO: when subtype? succeeds (returns true), we can safely save the resulting set of judgements that were shown to be consistent, for use during future calls to subtype?. Memoization essentially.

Returns:



35
36
37
38
39
40
41
42
43
44
 
# File 'lib/typisch/subtyping.rb', line 35

def subtype?(x, y, may_assume_proven = {}, depth=0)
  return true if may_assume_proven[[x,y]]
  may_assume_proven[[x,y]] = true

  result = check_subtype(x, y) do |u,v|
    subtype?(u, v, may_assume_proven, depth+1)
  end

  result
end

Instance Method Details

#<(other) ⇒ Object 



15
16
17
 
# File 'lib/typisch/type.rb', line 15

def <(other)
  self <= other && !(self >= other)
end

#<=(other) ⇒ Object 



11
12
13
 
# File 'lib/typisch/type.rb', line 11

def <=(other)
  Typisch::Type.subtype?(self, other)
end

#<=>(other) ⇒ Object 



42
43
44
45
46
47
48
 
# File 'lib/typisch/type.rb', line 42

def <=>(other)
  if other <= self
    self <= other ? 0 : 1
  else
    self <= other ? -1 : nil
  end
end

#==(other) ⇒ Object

N.B. equality is based on the subtyping algorithm. So, we cannot rely on using == on types inside any methods used in the subtyping algorithm. We must rely only on .equal? instance equality instead.

Note that we have not overridden hash and eql? to be compatible with this subtyping-based equality, since it’s not easy to find a unique representative of the equivalence class on which to base a hash function.

This means that hash lookup of types will remain based on instance equality, and can safely be used inside the subtyping logic without busting the stack



30
31
32
 
# File 'lib/typisch/type.rb', line 30

def ==(other)
  self <= other && self >= other
end

#===(instance, already_checked = {}) ⇒ Object

This uses essentially the same corecursive algorithm used for subtyping. Just this time we’re comparing with a possible instance rather than a possible subtype.



6
7
8
9
10
 
# File 'lib/typisch/type_checking.rb', line 6

def ===(instance, already_checked={})
  return true if already_checked[[self, instance]]
  already_checked[[self, instance]] = true
  check_type(instance) {|u,v| u.===(v, already_checked)}
end

#>(other) ⇒ Object 



38
39
40
 
# File 'lib/typisch/type.rb', line 38

def >(other)
  other < self
end

#>=(other) ⇒ Object 



34
35
36
 
# File 'lib/typisch/type.rb', line 34

def >=(other)
  other <= self
end

#alternative_types ⇒ Object

For convenience. Type::Constructor will implement this as [self], whereas Type::Union will implement it as its full list of alternative constructor types.

Raises:

  • (NotImplementedError) 


89
90
91
 
# File 'lib/typisch/type.rb', line 89

def alternative_types
  raise NotImplementedError
end

#annotations ⇒ Object

types may be annotated with a hash of arbitrary stuff. could use this to document them, or to add instructions for other tools which do type-directed metaprogramming.



79
80
81
 
# File 'lib/typisch/type.rb', line 79

def annotations
  @annotations ||= {}
end

#annotations=(annotations) ⇒ Object 



83
84
85
 
# File 'lib/typisch/type.rb', line 83

def annotations=(annotations)
  @annotations = annotations
end

#canonicalize! ⇒ Object

should update any references to subexpression types to point at their true target, eliminating any NamedPlaceholder wrappers.



101
102
 
# File 'lib/typisch/type.rb', line 101

def canonicalize!
end

#excluding_null ⇒ Object

returns a version of this type which excludes null. generally will be self, except when a union type which includes null.



124
125
126
 
# File 'lib/typisch/type.rb', line 124

def excluding_null
  self
end

#inspect ⇒ Object 



51
52
53
 
# File 'lib/typisch/type.rb', line 51

def inspect
  "#<Type: #{to_s}>"
end

#recursive?(found_so_far = {}) ⇒ Boolean

Does this type make any use of recursion / is it an ‘infinite’ type?

Returns:



105
106
107
108
109
110
111
112
113
 
# File 'lib/typisch/type.rb', line 105

def recursive?(found_so_far={})
  found_so_far[self] or begin
    found_so_far[self] = true
    result = subexpression_types.any? {|t| t.recursive?(found_so_far)}
#      subexpression_types.each {|t| raise t.inspect if t.recursive?(found_so_far)}
    found_so_far.delete(self)
    result
  end
end

#shallow_check_type(instance) ⇒ Object

should check the type of this instance, but only ‘one level deep’, ie typically just check its type tag without recursively type-checking any child objects.

Raises:

  • (NotImplementedError) 


118
119
120
 
# File 'lib/typisch/type.rb', line 118

def shallow_check_type(instance)
  raise NotImplementedError
end

#subexpression_types ⇒ Object

should return a list of any subexpressions which are themselves types. used by any generic type-graph-traversing logic.



95
96
97
 
# File 'lib/typisch/type.rb', line 95

def subexpression_types
  []
end

#target ⇒ Object

overridden on the Placeholder proxy wrapper, otherwise points at self



56
 
# File 'lib/typisch/type.rb', line 56

def target; self; end

#to_s(depth = 0, indent = '') ⇒ Object 



58
59
60
61
62
 
# File 'lib/typisch/type.rb', line 58

def to_s(depth=0, indent='')
  return @name.inspect if depth > 0 && @name
  return "..." if depth > 3 # MAX_DEPTH
  to_string(depth, indent)
end

#to_string(depth, indent) ⇒ Object

Raises:

  • (NotImplementedError) 


64
65
66
 
# File 'lib/typisch/type.rb', line 64

def to_string(depth, indent)
  raise NotImplementedError
end