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