Module: Dhall::TypeChecker

Defined in:
lib/dhall/typecheck.rb

Defined Under Namespace

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

Constant Summary collapse

KINDS = 
[
  Dhall::Variable["Type"],
  Dhall::Variable["Kind"],
  Dhall::Variable["Sort"]
].freeze
BUILTIN_TYPES = 
{
  "Natural/build"     => Dhall::Forall.of_arguments(
    Dhall::Forall.new(
      var:  "natural",
      type: Dhall::Variable["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: Dhall::Variable["Natural"]
  ),
  "Natural/fold"      => Dhall::Forall.of_arguments(
    Dhall::Variable["Natural"],
    body: Dhall::Forall.new(
      var:  "natural",
      type: Dhall::Variable["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/isZero"    => Dhall::Forall.of_arguments(
    Dhall::Variable["Natural"],
    body: Dhall::Variable["Bool"]
  ),
  "Natural/even"      => Dhall::Forall.of_arguments(
    Dhall::Variable["Natural"],
    body: Dhall::Variable["Bool"]
  ),
  "Natural/odd"       => Dhall::Forall.of_arguments(
    Dhall::Variable["Natural"],
    body: Dhall::Variable["Bool"]
  ),
  "Natural/toInteger" => Dhall::Forall.of_arguments(
    Dhall::Variable["Natural"],
    body: Dhall::Variable["Integer"]
  ),
  "Natural/show"      => Dhall::Forall.of_arguments(
    Dhall::Variable["Natural"],
    body: Dhall::Variable["Text"]
  ),
  "Text/show"         => Dhall::Forall.of_arguments(
    Dhall::Variable["Text"],
    body: Dhall::Variable["Text"]
  ),
  "List/build"        => Dhall::Forall.new(
    var:  "a",
    type: Dhall::Variable["Type"],
    body: Dhall::Forall.of_arguments(
      Dhall::Forall.new(
        var:  "list",
        type: Dhall::Variable["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: Dhall::Variable["List"],
        argument: Dhall::Variable["a"]
      )
    )
  ),
  "List/fold"         => Dhall::Forall.new(
    var:  "a",
    type: Dhall::Variable["Type"],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Dhall::Variable["List"],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Forall.new(
        var:  "list",
        type: Dhall::Variable["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: Dhall::Variable["Type"],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Dhall::Variable["List"],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Variable["Natural"]
    )
  ),
  "List/head"         => Dhall::Forall.new(
    var:  "a",
    type: Dhall::Variable["Type"],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Dhall::Variable["List"],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Application.new(
        function: Dhall::Variable["Optional"],
        argument: Dhall::Variable["a"]
      )
    )
  ),
  "List/last"         => Dhall::Forall.new(
    var:  "a",
    type: Dhall::Variable["Type"],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Dhall::Variable["List"],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Application.new(
        function: Dhall::Variable["Optional"],
        argument: Dhall::Variable["a"]
      )
    )
  ),
  "List/indexed"      => Dhall::Forall.new(
    var:  "a",
    type: Dhall::Variable["Type"],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Dhall::Variable["List"],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Application.new(
        function: Dhall::Variable["List"],
        argument: Dhall::RecordType.new(
          record: {
            "index" => Dhall::Variable["Natural"],
            "value" => Dhall::Variable["a"]
          }
        )
      )
    )
  ),
  "List/reverse"      => Dhall::Forall.new(
    var:  "a",
    type: Dhall::Variable["Type"],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Dhall::Variable["List"],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Application.new(
        function: Dhall::Variable["List"],
        argument: Dhall::Variable["a"]
      )
    )
  ),
  "Optional/fold"     => Dhall::Forall.new(
    var:  "a",
    type: Dhall::Variable["Type"],
    body: Dhall::Forall.of_arguments(
      Dhall::Application.new(
        function: Dhall::Variable["Optional"],
        argument: Dhall::Variable["a"]
      ),
      body: Dhall::Forall.new(
        var:  "optional",
        type: Dhall::Variable["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: Dhall::Variable["Type"],
    body: Dhall::Forall.of_arguments(
      Dhall::Forall.new(
        var:  "optional",
        type: Dhall::Variable["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: Dhall::Variable["Optional"],
        argument: Dhall::Variable["a"]
      )
    )
  ),
  "Integer/show"      => Dhall::Forall.of_arguments(
    Dhall::Variable["Integer"],
    body: Dhall::Variable["Text"]
  ),
  "Integer/toDouble"  => Dhall::Forall.of_arguments(
    Dhall::Variable["Integer"],
    body: Dhall::Variable["Double"]
  ),
  "Double/show"       => Dhall::Forall.of_arguments(
    Dhall::Variable["Double"],
    body: Dhall::Variable["Text"]
  )
}.freeze

Class Method Summary collapse

Class Method Details

.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
  raise TypeError, "#{message}: #{type}" unless assertion === type
  aexpr
end

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

Raises:

  • (TypeError) 


20
21
22
23
24
25
 
# 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
  raise TypeError, "#{message}: #{atype}, #{btype}" unless atype == btype
  atype
end

.for(expr) ⇒ Object

Raises:

  • (TypeError) 


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

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 



38
39
40
41
 
# File 'lib/dhall/typecheck.rb', line 38

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

.type_of(expr) ⇒ Object 



43
44
45
46
 
# File 'lib/dhall/typecheck.rb', line 43

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