This repository was archived by the owner on Mar 7, 2024. It is now read-only.
This repository was archived by the owner on Mar 7, 2024. It is now read-only.
unwraps and panics #303Open
Description
Hacspec has one unique AST which is shared at different stages.
A stage typically expects its input AST to be of a particular shape, e.g., have type information, or have its name resolved.
However, for now, the type of Hacspec ASTs (Expressions, Statements, Blocks, etc.) is the same at every stage. Hence, we have no way of guaranteeing that, e.g., after type checking, every node has type information. This results in various unsafe unwraps and panic!s.
That would be nice to have some kind of GADT to ensure such things on type-level.
Rust has no actual support for GADT, but with traits and the never type, we can do things already, for instance:
Example
#![feature(never_type)]
pub mod levels {
pub struct Untyped;
pub struct Typed;
pub struct Elaborated;
}
pub trait Features {
type HasQuestionMark;
type HasMonadicLet;
type TypInfo<T>;
}
impl Features for levels::Untyped {
type HasQuestionMark = ();
type HasMonadicLet = !;
type TypInfo<T> = std::marker::PhantomData<T>;
}
impl Features for levels::Typed {
type HasQuestionMark = ();
type HasMonadicLet = !;
type TypInfo<T> = T;
}
impl Features for levels::Elaborated {
type HasQuestionMark = !;
type HasMonadicLet = ();
type TypInfo<T> = T;
}
pub type Ident = String;
pub enum Typ {
DummyType
}
pub enum Expression<Lvl: Features> {
MonadicLet(Lvl::HasMonadicLet/*, other fields... */),
QuestionMark(Lvl::HasQuestionMark/*, other fields... */),
Named(Ident, Lvl::TypInfo<Typ>),
// other stuff...
}
use Expression::*;
pub fn typecheck_expression(e: Expression<levels::Untyped>) -> Expression<levels::Typed> {
match e {
MonadicLet(never) => never, // `never` has type `!`, thus: `never` is castable to any type
QuestionMark(() /*other stuff*/) => QuestionMark(() /*...*/),
Named(x, _) => Named(x, Typ::DummyType)
}
}
pub fn elaborate_expression(e: Expression<levels::Typed>) -> Expression<levels::Elaborated> {
match e {
MonadicLet(never) => never,
QuestionMark(()) => MonadicLet(()),
Named(x, Typ::DummyType) => Named(x, Typ::DummyType)
}
}