Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement type system for Bend #679

Open
16 tasks done
kings177 opened this issue Aug 19, 2024 · 2 comments
Open
16 tasks done

Implement type system for Bend #679

kings177 opened this issue Aug 19, 2024 · 2 comments
Assignees
Labels
compilation Compilation of terms and functions to HVM enhancement New feature or request

Comments

@kings177
Copy link
Member

kings177 commented Aug 19, 2024

#615 describes the need for having a type system for Bend as well as the design discussion of how this system should be.

This issue tracks the implementation of the bend type system.

  • Compile bend programs to kindc, deferring type checking to kind.
  • Study the implementation of Hindley-Milner type systems.
  • Search for extensions and alternatives to HM that could allow for a less restrictive set of accepted lambda terms.
  • Implement a simple HM type system with type inference.
  • Add recursion to the type system.
  • Add adts to the type system.
  • Add mutual recursion to the type system.
  • Port the type system from haskell to rust.
  • Port the implemented type system to Bend.
  • Add the Bend-specific types to the type system (numbers, tuples, None).
  • Add type checking, comparing with user provided annotations.
  • Add non-checked functions.
  • Add the untyped type Any.
  • Write good type error diagnostics.
  • Update the builtin library to use the new type system correctly.
  • Write tests for type inference and type checking.
@developedby developedby changed the title Transferring Haskell Type Systems to Rust Implement type system for Bend Aug 20, 2024
@developedby
Copy link
Member

Using kindc as the type checker for Bend does work to an extend, correctly checking the functions, but the unification algorithm is quite limited in what it can infer, needing a great deal of help with annotations or by breaking things in smaller chunks.

For kind users that is not such a big problem, since they get full access to the underlying type system, but for Bend a lot of the problematic things come from the compilation process itself, either from generated functions/terms or from the conversion of Bend to kindc.

It would be bad UX if Bend users also needed to understand the limitations of the kindc checker. So I decided it'd be better to instead implement our own actual HM type system which, since it's much more restricted in what it can do, doesn't hit the same issues.

@developedby
Copy link
Member

Directly writing the type system in the bend codebase was a bit too hard since it has too many things already that need to be taken care of to even compile the most basic things.

So I decided it'd be better to first implement it in a separate repo and after I had the basic stuff down I'd port it back to Bend. Writing it directly in Rust was also a bit hard since most (legible, well-structured) implementations use a very functional style. Rust also needs a lot more boilerplate which hurt the legibility that I needed to learn how HM works and how to implement it.

I'm first implementing it in haskell in that same repo, then converting things to Rust and then finally to Bend.

@kings177 kings177 modified the milestone: Type system Aug 20, 2024
@developedby developedby added compilation Compilation of terms and functions to HVM enhancement New feature or request labels Aug 21, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
compilation Compilation of terms and functions to HVM enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

2 participants