From 130de8cea49c848a06174c61c747d9414a5c71b7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 16 Feb 2020 19:06:23 +0000 Subject: Start requiring Universe to build a Type --- dhall/src/semantics/tck/tyexpr.rs | 117 +++++++++++++--- dhall/src/semantics/tck/typecheck.rs | 263 ++++++++++++++--------------------- 2 files changed, 205 insertions(+), 175 deletions(-) (limited to 'dhall/src/semantics/tck') diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 4999899..3c47a81 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,8 +1,12 @@ -use crate::error::TypeError; -use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value, ValueKind, VarEnv}; +use crate::error::{ErrorBuilder, TypeError}; +use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv}; use crate::syntax::{Builtin, Const, Span}; use crate::{NormalizedExpr, ToExprOptions}; +/// The type of a type. 0 is `Type`, 1 is `Kind`, etc... +#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)] +pub(crate) struct Universe(u8); + /// An expression representing a type #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) struct Type { @@ -16,12 +20,64 @@ pub(crate) struct TyExpr { ty: Type, } +impl Universe { + pub fn from_const(c: Const) -> Self { + Universe(match c { + Const::Type => 0, + Const::Kind => 1, + Const::Sort => 2, + }) + } + pub fn as_const(self) -> Option { + match self.0 { + 0 => Some(Const::Type), + 1 => Some(Const::Kind), + 2 => Some(Const::Sort), + _ => None, + } + } + pub fn next(self) -> Self { + Universe(self.0 + 1) + } + pub fn previous(self) -> Option { + if self.0 == 0 { + None + } else { + Some(Universe(self.0 - 1)) + } + } +} + impl Type { + pub fn new(val: Value, _u: Universe) -> Self { + Type { val } + } pub fn from_const(c: Const) -> Self { - Value::from_const(c).into() + Self::new(Value::from_const(c), c.to_universe().next()) } pub fn from_builtin(b: Builtin) -> Self { - Value::from_builtin(b).into() + use Builtin::*; + match b { + Bool | Natural | Integer | Double | Text => {} + _ => unreachable!("this builtin is not a type: {}", b), + } + + Self::new(Value::from_builtin(b), Universe::from_const(Const::Type)) + } + + /// Get the type of this type + // TODO: avoid recomputing so much + pub fn ty(&self, env: &TyEnv) -> Result, TypeError> { + Ok(self.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const()) + } + /// Get the type of this type + // TODO: avoid recomputing so much + pub fn ty_univ(&self, env: &TyEnv) -> Result { + Ok(match self.ty(env)? { + Some(c) => c.to_universe(), + // TODO: hack, might explode + None => Const::Sort.to_universe().next(), + }) } pub fn to_value(&self) -> Value { @@ -49,9 +105,9 @@ impl Type { } impl TyExpr { - pub fn new(kind: HirKind, ty: Type, span: Span) -> Self { + pub fn from_hir(hir: &Hir, ty: Type) -> Self { TyExpr { - hir: Hir::new(kind, span), + hir: hir.clone(), ty, } } @@ -62,16 +118,6 @@ impl TyExpr { pub fn ty(&self) -> &Type { &self.ty } - /// Get the kind (the type of the type) of this value - // TODO: avoid recomputing so much - pub fn get_kind(&self, env: &TyEnv) -> Result, TypeError> { - Ok(self - .ty() - .to_hir(env.as_varenv()) - .typecheck(env)? - .ty() - .as_const()) - } pub fn to_hir(&self) -> Hir { self.as_hir().clone() @@ -79,18 +125,51 @@ impl TyExpr { pub fn as_hir(&self) -> &Hir { &self.hir } - /// Converts a value back to the corresponding AST expression. + /// Converts a closed expression back to the corresponding AST expression. pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { self.as_hir().to_expr(opts) } + pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { + self.as_hir().to_expr_tyenv(env) + } /// Eval the TyExpr. It will actually get evaluated only as needed on demand. pub fn eval(&self, env: impl Into) -> Value { self.as_hir().eval(env.into()) } + pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> { + if self.ty().as_const().is_none() { + return mkerr( + ErrorBuilder::new(format!( + "Expected a type, found: `{}`", + self.to_expr_tyenv(env), + )) + .span_err( + self.span(), + format!( + "this has type: `{}`", + self.ty().to_expr_tyenv(env) + ), + ) + .help(format!( + "An expression in type position must have type `Type`, \ + `Kind` or `Sort`", + )) + .format(), + ); + } + Ok(()) + } /// Evaluate to a Type. - pub fn eval_to_type(&self, env: impl Into) -> Type { - self.eval(env).into() + pub fn eval_to_type(&self, env: &TyEnv) -> Result { + self.ensure_is_type(env)?; + Ok(Type::new( + self.eval(env), + self.ty() + .as_const() + .expect("case handled in ensure_is_type") + .to_universe(), + )) } /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as /// needed on demand. diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index dd996ae..1281045 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -15,8 +15,8 @@ use crate::syntax::{ fn check_rectymerge( span: &Span, env: &TyEnv, - x: Type, - y: Type, + x: Value, + y: Value, ) -> Result<(), TypeError> { let kts_x = match x.kind() { ValueKind::RecordType(kts) => kts, @@ -39,7 +39,7 @@ fn check_rectymerge( for (k, tx) in kts_x { if let Some(ty) = kts_y.get(k) { // TODO: store Type in RecordType ? - check_rectymerge(span, env, tx.clone().into(), ty.clone().into())?; + check_rectymerge(span, env, tx.clone(), ty.clone())?; } } Ok(()) @@ -70,9 +70,8 @@ pub fn mk_span_err(span: Span, msg: S) -> Result { fn type_one_layer( env: &TyEnv, ekind: ExprKind, - annot: Option, span: Span, -) -> Result { +) -> Result { let span_err = |msg: &str| mk_span_err(span.clone(), msg); let ty = match &ekind { @@ -81,84 +80,19 @@ fn type_one_layer( } ExprKind::Var(..) | ExprKind::Const(Const::Sort) + | ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) | ExprKind::Annot(..) => { unreachable!("This case should have been handled in type_with") } - ExprKind::Lam(binder, annot, body) => { - if annot.ty().as_const().is_none() { - return mkerr( - ErrorBuilder::new(format!( - "Invalid input type: `{}`", - annot.ty().to_expr_tyenv(env), - )) - .span_err( - annot.span(), - format!( - "this has type: `{}`", - annot.ty().to_expr_tyenv(env) - ), - ) - .help(format!( - "The input type of a function must have type `Type`, \ - `Kind` or `Sort`", - )) - .format(), - ); - } - let body_env = env.insert_type(&binder, annot.eval_to_type(env)); - if body.get_kind(&body_env)?.is_none() { - return span_err("Invalid output type"); - } - Hir::new( - HirKind::Expr(ExprKind::Pi( - binder.clone(), - annot.to_hir(), - body.ty().to_hir(body_env.as_varenv()), - )), - span.clone(), - ) - .eval_to_type(env) - } - ExprKind::Pi(_, annot, body) => { - let ks = match annot.ty().as_const() { - Some(k) => k, - _ => { - return mkerr( - ErrorBuilder::new(format!( - "Invalid input type: `{}`", - annot.ty().to_expr_tyenv(env), - )) - .span_err( - annot.span(), - format!( - "this has type: `{}`", - annot.ty().to_expr_tyenv(env) - ), - ) - .help(format!( - "The input type of a function must have type \ - `Type`, `Kind` or `Sort`", - )) - .format(), - ); - } - }; - let kt = match body.ty().as_const() { - Some(k) => k, - _ => return span_err("Invalid output type"), - }; - - Type::from_const(function_check(ks, kt)) - } - ExprKind::Let(_, _, _, body) => body.ty().clone(), - ExprKind::Const(Const::Type) => Type::from_const(Const::Kind), ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort), ExprKind::Builtin(b) => { let t_hir = type_of_builtin(*b); let t_tyexpr = typecheck(&t_hir)?; - t_tyexpr.eval_to_type(env) + t_tyexpr.eval_to_type(env)? } ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool), ExprKind::Lit(LitKind::Natural(_)) => { @@ -183,7 +117,7 @@ fn type_one_layer( text_type } ExprKind::EmptyListLit(t) => { - let t = t.eval_to_type(env); + let t = t.eval_to_type(env)?; match t.kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, @@ -202,7 +136,7 @@ fn type_one_layer( return span_err("InvalidListElement"); } } - if x.get_kind(env)? != Some(Const::Type) { + if x.ty().ty(env)? != Some(Const::Type) { return span_err("InvalidListType"); } @@ -210,7 +144,7 @@ fn type_one_layer( Value::from_builtin(Builtin::List).app(t).to_type() } ExprKind::SomeLit(x) => { - if x.get_kind(env)? != Some(Const::Type) { + if x.ty().ty(env)? != Some(Const::Type) { return span_err("InvalidOptionalType"); } @@ -230,7 +164,7 @@ fn type_one_layer( }; // Check that the fields have a valid kind - match v.get_kind(env)? { + match v.ty().ty(env)? { Some(_) => {} None => return span_err("InvalidFieldType"), } @@ -297,7 +231,7 @@ fn type_one_layer( }, // TODO: branch here only when scrut.ty() is a Const _ => { - let scrut_nf = scrut.eval_to_type(env); + let scrut_nf = scrut.eval(env); match scrut_nf.kind() { ValueKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > @@ -305,13 +239,11 @@ fn type_one_layer( Value::from_kind(ValueKind::PiClosure { binder: Binder::new(x.clone()), annot: ty.clone(), - closure: Closure::new_constant( - scrut_nf.into_value(), - ), + closure: Closure::new_constant(scrut_nf), }) .to_type() } - Some(None) => scrut_nf, + Some(None) => scrut_nf.to_type(), None => return span_err("MissingUnionField"), }, _ => return span_err("NotARecord"), @@ -320,7 +252,7 @@ fn type_one_layer( } } ExprKind::Assert(t) => { - let t = t.eval_to_type(env); + let t = t.eval_to_type(env)?; match t.kind() { ValueKind::Equivalence(x, y) if x == y => {} ValueKind::Equivalence(..) => { @@ -382,7 +314,7 @@ fn type_one_layer( if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } - if y.get_kind(env)? != Some(Const::Type) { + if y.ty().ty(env)? != Some(Const::Type) { return span_err("IfBranchMustBeTerm"); } if y.ty() != z.ty() { @@ -415,25 +347,22 @@ fn type_one_layer( Value::from_kind(ValueKind::RecordType(kts)).to_type() } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { - check_rectymerge(&span, env, x.ty().clone(), y.ty().clone())?; + check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?; - Hir::new( + let hir = Hir::new( HirKind::Expr(ExprKind::BinOp( BinOp::RecursiveRecordTypeMerge, x.ty().to_hir(env.as_varenv()), y.ty().to_hir(env.as_varenv()), )), span.clone(), - ) - .eval_to_type(env) + ); + let x_u = x.ty().ty_univ(env)?; + let y_u = y.ty().ty_univ(env)?; + Type::new(hir.eval(env), max(x_u, y_u)) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { - check_rectymerge( - &span, - env, - x.eval_to_type(env), - y.eval_to_type(env), - )?; + check_rectymerge(&span, env, x.eval(env), y.eval(env))?; // A RecordType's type is always a const let xk = x.ty().as_const().unwrap(); @@ -459,7 +388,7 @@ fn type_one_layer( if l.ty() != r.ty() { return span_err("EquivalenceTypeMismatch"); } - if l.get_kind(env)? != Some(Const::Type) { + if l.ty().ty(env)? != Some(Const::Type) { return span_err("EquivalenceArgumentsMustBeTerms"); } @@ -614,7 +543,10 @@ fn type_one_layer( } } - let type_annot = type_annot.as_ref().map(|t| t.eval_to_type(env)); + let type_annot = type_annot + .as_ref() + .map(|t| t.eval_to_type(env)) + .transpose()?; match (inferred_type, type_annot) { (Some(t1), Some(t2)) => { if t1 != t2 { @@ -628,7 +560,7 @@ fn type_one_layer( } } ExprKind::ToMap(record, annot) => { - if record.get_kind(env)? != Some(Const::Type) { + if record.ty().ty(env)? != Some(Const::Type) { return span_err("`toMap` only accepts records of type `Type`"); } let record_t = record.ty(); @@ -648,7 +580,7 @@ fn type_one_layer( annotation", ); }; - let annot_val = annot.eval_to_type(env); + let annot_val = annot.eval_to_type(env)?; let err_msg = "The type of `toMap x` must be of the form \ `List { mapKey : Text, mapValue : T }`"; @@ -693,7 +625,7 @@ fn type_one_layer( .app(Value::from_kind(ValueKind::RecordType(kts))) .to_type(); if let Some(annot) = annot { - let annot_val = annot.eval_to_type(env); + let annot_val = annot.eval_to_type(env)?; if output_type != annot_val { return span_err("Annotation mismatch"); } @@ -733,7 +665,7 @@ fn type_one_layer( _ => return span_err("ProjectionMustBeRecord"), }; - let selection_val = selection.eval_to_type(env); + let selection_val = selection.eval_to_type(env)?; let sel_kts = match selection_val.kind() { ValueKind::RecordType(kts) => kts, _ => return span_err("ProjectionByExprTakesRecordType"), @@ -754,22 +686,7 @@ fn type_one_layer( } }; - if let Some(annot) = annot { - if ty != annot { - return span_err(&format!( - "annot mismatch: {} != {}", - ty.to_expr_tyenv(env), - annot.to_expr_tyenv(env) - )); - } - } - - // TODO: avoid retraversing - Ok(TyExpr::new( - HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())), - ty, - span, - )) + Ok(ty) } /// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation @@ -779,59 +696,93 @@ pub(crate) fn type_with( hir: &Hir, annot: Option, ) -> Result { - match hir.kind() { - HirKind::Var(var) => { - Ok(TyExpr::new(HirKind::Var(*var), env.lookup(var), hir.span())) - } + let tyexpr = match hir.kind() { + HirKind::Var(var) => TyExpr::from_hir(hir, env.lookup(var)), HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } HirKind::Expr(ExprKind::Const(Const::Sort)) => { - mk_span_err(hir.span(), "Sort does not have a type") + return mk_span_err(hir.span(), "Sort does not have a type") } HirKind::Expr(ExprKind::Annot(x, t)) => { let t = match t.kind() { HirKind::Expr(ExprKind::Const(Const::Sort)) => { Type::from_const(Const::Sort) } - _ => type_with(env, t, None)?.eval_to_type(env), + _ => type_with(env, t, None)?.eval_to_type(env)?, }; - type_with(env, x, Some(t)) + type_with(env, x, Some(t))? } - HirKind::Expr(ekind) => { - let ekind = match ekind { - ExprKind::Lam(binder, annot, body) => { - let annot = type_with(env, annot, None)?; - let annot_nf = annot.eval_to_type(env); - let body_env = env.insert_type(binder, annot_nf); - let body = type_with(&body_env, body, None)?; - ExprKind::Lam(binder.clone(), annot, body) - } - ExprKind::Pi(binder, annot, body) => { - let annot = type_with(env, annot, None)?; - let annot_val = annot.eval_to_type(env); - let body_env = env.insert_type(binder, annot_val); - let body = type_with(&body_env, body, None)?; - ExprKind::Pi(binder.clone(), annot, body) - } - ExprKind::Let(binder, annot, val, body) => { - let val_annot = if let Some(t) = annot { - Some(type_with(env, t, None)?.eval_to_type(env)) - } else { - None - }; - let val = type_with(env, &val, val_annot)?; - let val_nf = val.eval(env); - let body_env = - env.insert_value(&binder, val_nf, val.ty().clone()); - let body = type_with(&body_env, body, None)?; - ExprKind::Let(binder.clone(), None, val, body) - } - _ => ekind.traverse_ref(|e| type_with(env, e, None))?, + + HirKind::Expr(ExprKind::Lam(binder, annot, body)) => { + let annot = type_with(env, annot, None)?; + let annot_nf = annot.eval_to_type(env)?; + let body_env = env.insert_type(binder, annot_nf); + let body = type_with(&body_env, body, None)?; + + let u_annot = annot.ty().as_const().unwrap(); + let u_body = match body.ty().ty(&body_env)? { + Some(k) => k, + _ => return mk_span_err(hir.span(), "Invalid output type"), }; - type_one_layer(env, ekind, annot, hir.span()) + let u = function_check(u_annot, u_body).to_universe(); + let ty_hir = Hir::new( + HirKind::Expr(ExprKind::Pi( + binder.clone(), + annot.to_hir(), + body.ty().to_hir(body_env.as_varenv()), + )), + hir.span(), + ); + let ty = Type::new(ty_hir.eval(env), u); + + TyExpr::from_hir(hir, ty) + } + HirKind::Expr(ExprKind::Pi(binder, annot, body)) => { + let annot = type_with(env, annot, None)?; + let annot_val = annot.eval_to_type(env)?; + let body_env = env.insert_type(binder, annot_val); + let body = type_with(&body_env, body, None)?; + body.ensure_is_type(env)?; + + let ks = annot.ty().as_const().unwrap(); + let kt = body.ty().as_const().unwrap(); + let ty = Type::from_const(function_check(ks, kt)); + TyExpr::from_hir(hir, ty) + } + HirKind::Expr(ExprKind::Let(binder, annot, val, body)) => { + let val_annot = annot + .as_ref() + .map(|t| Ok(type_with(env, t, None)?.eval_to_type(env)?)) + .transpose()?; + let val = type_with(env, &val, val_annot)?; + let val_nf = val.eval(env); + let body_env = env.insert_value(&binder, val_nf, val.ty().clone()); + let body = type_with(&body_env, body, None)?; + let ty = body.ty().clone(); + TyExpr::from_hir(hir, ty) + } + HirKind::Expr(ekind) => { + let ekind = ekind.traverse_ref(|e| type_with(env, e, None))?; + let ty = type_one_layer(env, ekind, hir.span())?; + TyExpr::from_hir(hir, ty) + } + }; + + if let Some(annot) = annot { + if *tyexpr.ty() != annot { + return mk_span_err( + hir.span(), + &format!( + "annot mismatch: {} != {}", + tyexpr.ty().to_expr_tyenv(env), + annot.to_expr_tyenv(env) + ), + ); } } + + Ok(tyexpr) } /// Typecheck an expression and return the expression annotated with types if type-checking @@ -842,6 +793,6 @@ pub(crate) fn typecheck(hir: &Hir) -> Result { /// Like `typecheck`, but additionally checks that the expression's type matches the provided type. pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result { - let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new()); + let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?; type_with(&TyEnv::new(), hir, Some(ty)) } -- cgit v1.2.3