raffopazzo / depc

Like C and C++ but with Dependent Types
1 stars 1 forks source link

Add type_t with share semantics #53

Open raffopazzo opened 1 month ago

raffopazzo commented 1 month ago

Many expressions have the same type, for example all entries in an array but more complex examples are also possible. We could then allow all these expressions to share the same type by introducing some smart wrapper around shared_ptr<expr_t> along the lines of

class type_t
{
    std::shared_ptr<expr_t> value;
public:
    explicit type_t(expr_t const&);
    expr_t& operator*();
    expr_t const& operator*() const;
};

This would reduce the memory footprint of types and perform beta-reduction only once.

raffopazzo commented 4 days ago

I gave this a go but it's probably not straightforward. For example should func_arg_t::type be a type_t? Intuitively yes. Then likewise for pi_t::ret_type and abs_t::ret_type but an array is really just app_t of array_t and a type expression for the element type, which should technically be a type_t but it can't since it's inside an app_t. The whole thing may become highly confusing and hard to manage. So for now better park this idea and reassess in future whether this is really worth pursuing.