Module: Dhall::TypeChecker

Defined in:
lib/dhall/typecheck.rb

Defined Under Namespace

Classes: AnonymousType, Application, Assertion, Builtin, Context, EmptyAnonymousType, EmptyList, EmptyRecord, Enum, Forall, Function, If, LetIn, LetInAnnotated, List, Literal, Merge, Operator, OperatorEquivalent, OperatorListConcatenate, OperatorRecursiveRecordMerge, OperatorRecursiveRecordTypeMerge, OperatorRightBiasedRecordMerge, Optional, OptionalNone, Record, RecordProjection, RecordProjectionByExpression, RecordSelection, TextLiteral, ToMap, TypeAnnotation, Union, UnionType, Variable

Constant Summary collapse

KINDS = 
[
  Builtins[:Type],
  Builtins[:Kind],
  Builtins[:Sort]
].freeze
BUILTIN_TYPES = 
{
  "Bool"              => Builtins[:Type],
  "Type"              => Builtins[:Kind],
  "Kind"              => Builtins[:Sort],
  "Natural"           => Builtins[:Type],
  "Integer"           => Builtins[:Type],
  "Double"            => Builtins[:Type],
  "Text"              => Builtins[:Type],
  "List"              => Dhall::Forall.of_arguments(
    Builtins[:Type],
    body: Builtins[:Type]
  ),
  "Optional"          => Dhall::Forall.of_arguments(
    Builtins[:Type],
    body: Builtins[:Type]
  ),
  "None"              => Dhall::Forall.new(
    var:  "A",
    type: Builtins[:Type],
    body: Dhall::Application.new(
      function: Builtins[:Optional],
      argument: Dhall::Variable["A"]
    )
  ),
  "Natural/build"     => Dhall::Forall.of_arguments(
    Dhall::Forall.new(
      var:  "natural",
      type: Builtins[:Type],
      body: Dhall::Forall.new(
        var:  "succ",
        type: Dhall::Forall.of_arguments(
          Dhall::Variable["natural"],
          body: Dhall::Variable["natural"]
        ),
        body: Dhall::Forall.new(
          var:  "zero",
          type: Dhall::Variable["natural"],
          body: Dhall::Variable["natural"]
        )
      )
    ),
    body: Builtins[:Natural]
  ),
  "Natural/fold"      => Dhall::Forall.of_arguments(
    Builtins[:Natural],
    body: Dhall::Forall.new(
      var:  "natural",
      type: Builtins[:Type],
      body: Dhall::Forall.new(
        var:  "succ",
        type: Dhall::Forall.of_arguments(
          Dhall::Variable["natural"],
          body: Dhall::Variable["natural"]
        ),
        body: Dhall::Forall.new(
          var:  "zero",
          type: Dhall::Variable["natural"],
          body: Dhall::Variable["natural"]
        )
      )
    )
  ),
  "Natural/subtract"  => Dhall::Forall.of_arguments(
    Builtins[:Natural],
    Builtins[:Natural],
    body: Builtins[:Natural]
  ),
  "Natural/isZero"    => Dhall::Forall.of_arguments(
    Builtins[:Natural],
    body: Builtins[:Bool]
  ),
  "Natural/even"      => Dhall::Forall.of_arguments(
    Builtins[:Natural],
    body: Builtins[:Bool]
  ),
  "Natural/odd"       => Dhall::Forall.of_arguments(
    Builtins[:Natural],
    body: Builtins[:Bool]
  ),
  "Natural/toInteger" => Dhall::Forall.of_arguments(
    Builtins[:Natural],
    body: Builtins[:Integer]
  ),
  "Natural/show"      => Dhall::Forall.of_arguments(
    Builtins[:Natural],
    body: Builtins[:Text]
  ),
  "Text/show"         => Dhall::Forall.of_arguments(
    Builtins[:Text],
    body: Builtins[:Text]
  ),
  "List/build"        => Dhall::Forall.new(
    var:  "a",
    type: Builtins[:Type],
    body: Dhall::Forall.of_arguments(
      Dhall::Forall.new(
        var:  "list",
        type: Builtins[:Type],
        body: Dhall::Forall.new(
          var:  "cons",
          type: Dhall::Forall.of_arguments(
            Dhall::Variable["a"],
            Dhall::Variable["list"],
            body: Dhall::Variable["list"]
          ),
          body: Dhall::Forall.new(
            var:  "nil",
            type: Dhall::Variable["list"],
            body: Dhall::Variable["list"]
          )
        )
      ),
      body: Dhall::Application.new(
        function: Builtins[:List],
        argument: Dhall::Variable["a"]
      )
    )
  ),
  "List/fold"         => Dhall::Forall.new(
    var:  "a",
    type: Builtins[:Type],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Builtins[:List],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Forall.new(
        var:  "list",
        type: Builtins[:Type],
        body: Dhall::Forall.new(
          var:  "cons",
          type: Dhall::Forall.of_arguments(
            Dhall::Variable["a"],
            Dhall::Variable["list"],
            body: Dhall::Variable["list"]
          ),
          body: Dhall::Forall.new(
            var:  "nil",
            type: Dhall::Variable["list"],
            body: Dhall::Variable["list"]
          )
        )
      )
    )
  ),
  "List/length"       => Dhall::Forall.new(
    var:  "a",
    type: Builtins[:Type],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Builtins[:List],
        argument: Dhall::Variable["a"]
      ),
      body: Builtins[:Natural]
    )
  ),
  "List/head"         => Dhall::Forall.new(
    var:  "a",
    type: Builtins[:Type],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Builtins[:List],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Application.new(
        function: Builtins[:Optional],
        argument: Dhall::Variable["a"]
      )
    )
  ),
  "List/last"         => Dhall::Forall.new(
    var:  "a",
    type: Builtins[:Type],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Builtins[:List],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Application.new(
        function: Builtins[:Optional],
        argument: Dhall::Variable["a"]
      )
    )
  ),
  "List/indexed"      => Dhall::Forall.new(
    var:  "a",
    type: Builtins[:Type],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Builtins[:List],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Application.new(
        function: Builtins[:List],
        argument: Dhall::RecordType.new(
          record: {
            "index" => Builtins[:Natural],
            "value" => Dhall::Variable["a"]
          }
        )
      )
    )
  ),
  "List/reverse"      => Dhall::Forall.new(
    var:  "a",
    type: Builtins[:Type],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Builtins[:List],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Application.new(
        function: Builtins[:List],
        argument: Dhall::Variable["a"]
      )
    )
  ),
  "Optional/fold"     => Dhall::Forall.new(
    var:  "a",
    type: Builtins[:Type],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Builtins[:Optional],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Forall.new(
        var:  "optional",
        type: Builtins[:Type],
        body: Dhall::Forall.new(
          var:  "just",
          type: Dhall::Forall.of_arguments(
            Dhall::Variable["a"],
            body: Dhall::Variable["optional"]
          ),
          body: Dhall::Forall.new(
            var:  "nothing",
            type: Dhall::Variable["optional"],
            body: Dhall::Variable["optional"]
          )
        )
      )
    )
  ),
  "Optional/build"    => Dhall::Forall.new(
    var:  "a",
    type: Builtins[:Type],
    body: Dhall::Forall.of_arguments(
      Dhall::Forall.new(
        var:  "optional",
        type: Builtins[:Type],
        body: Dhall::Forall.new(
          var:  "just",
          type: Dhall::Forall.of_arguments(
            Dhall::Variable["a"],
            body: Dhall::Variable["optional"]
          ),
          body: Dhall::Forall.new(
            var:  "nothing",
            type: Dhall::Variable["optional"],
            body: Dhall::Variable["optional"]
          )
        )
      ),
      body: Dhall::Application.new(
        function: Builtins[:Optional],
        argument: Dhall::Variable["a"]
      )
    )
  ),
  "Integer/show"      => Dhall::Forall.of_arguments(
    Builtins[:Integer],
    body: Builtins[:Text]
  ),
  "Integer/toDouble"  => Dhall::Forall.of_arguments(
    Builtins[:Integer],
    body: Builtins[:Double]
  ),
  "Double/show"       => Dhall::Forall.of_arguments(
    Builtins[:Double],
    body: Builtins[:Text]
  )
}.freeze

Class Method Summary collapse

Class Method Details

.annotate(expr) ⇒ Object 



45
46
47
48
 
# File 'lib/dhall/typecheck.rb', line 45

def self.annotate(expr)
  return if expr.nil?
  TypeChecker.for(expr).annotate(TypeChecker::Context.new)
end

.assert(type, assertion, message) ⇒ Object

Raises:

  • (TypeError) 


8
9
10
11
 
# File 'lib/dhall/typecheck.rb', line 8

def self.assert(type, assertion, message)
  raise TypeError, message unless assertion === type
  type
end

.assert_type(expr, assertion, message, context:) ⇒ Object

Raises:

  • (TypeError) 


13
14
15
16
17
18
 
# File 'lib/dhall/typecheck.rb', line 13

def self.assert_type(expr, assertion, message, context:)
  aexpr = self.for(expr).annotate(context)
  type = aexpr.type.normalize
  raise TypeError, "#{message}: #{type}" unless assertion === type
  aexpr
end

.assert_types_match(a, b, message, context:) ⇒ Object 



20
21
22
23
24
25
26
27
 
# File 'lib/dhall/typecheck.rb', line 20

def self.assert_types_match(a, b, message, context:)
  atype = self.for(a).annotate(context).type
  btype = self.for(b).annotate(context).type
  unless atype.normalize == btype.normalize
    raise TypeError, "#{message}: #{atype}, #{btype}"
  end
  atype
end

.for(expr) ⇒ Object

Raises:

  • (TypeError) 


29
30
31
32
33
34
35
36
37
38
 
# File 'lib/dhall/typecheck.rb', line 29

def self.for(expr)
  @typecheckers.each do |node_matcher, (typechecker, extras)|
    if node_matcher === expr
      msg = [:call, :for, :new].find { |m| typechecker.respond_to?(m) }
      return typechecker.public_send(msg, expr, *extras)
    end
  end

  raise TypeError, "Unknown expression: #{expr.inspect}"
end

.register(typechecker, node_type, *extras) ⇒ Object 



40
41
42
43
 
# File 'lib/dhall/typecheck.rb', line 40

def self.register(typechecker, node_type, *extras)
  @typecheckers ||= {}
  @typecheckers[node_type] ||= [typechecker, extras]
end

.type_of(expr) ⇒ Object 



50
51
52
 
# File 'lib/dhall/typecheck.rb', line 50

def self.type_of(expr)
  annotate(expr)&.type
end