search

Cypher1 / tako

An experimental programming language for ergonomic software verification
https://takolang.dev
MIT License
15 stars 1 forks source link

Struct like records / Compact Algebraic Data types #50

Open Cypher1 opened 5 years ago

Cypher1 commented 5 years ago

Building on #48 there should be a simple way to build more complex data structures that support tagging (at compile time where possible).

Ideally these would be subtypable (i.e. Left a and Right b a subtypes of Either a b and do not need to be defined separately). This should make typing guarantees more useful without requiring common Haskell patterns such as data Value = IntV Int | BoolV Bool. Instead it should be possible to have a type Value = Int | Bool, only requiring clarification when those types overlap.

Cypher1 commented 5 years ago

Work on this has progressed substantially in https://github.com/Cypher1/Tako/pull/72 but the PrimOpTypes still need to be converted to use the new data types, as does the interpreter.

This should allow the start of work on code generation and exploration of unification of Tako's two type checkers (one for data and one for predicates).

Cypher1 commented 5 years ago

A small subset of common operations on bit vectors are available and a bool/bit, uint 'shaped' bit vectors available. Basic maths operations and bit shifting a not yet available.