Dependent types

[TropicSapling]

Inspired by Agda, allow you to define types not only based on other types but also based on values. Supposedly this should somehow allow the compiler to report more mistakes at compile time, not sure how to make that work though? I guess in the example code below it might just work?

Possible syntax?:

func new_array (Array arr) -> Array<_> {
     (Array<arr length>) arr
}

func double_arr (Array<len> arr) -> Array<len * 2> {
    ...
}

func requires_array3(Array<3> arr) -> ... {
    ...
}

func init {
    let arr = new_array [1 2 3];
    let new_arr = double_arr arr; // {1, 2, 3, 1, 2, 3}
    
    requires_array3 arr; // works
    requires_array3 new_arr; // ERROR: 'Array<6>' is not same type as 'Array<3>'
}

Perhaps a better example:

func smash (Array<len> arr) (Array<len2> arr2) -> Array<len + len2> {
    ...
}

[TropicSapling]

Alt. syntax if using arg pattern matching:

func new_array (Array arr) -> Array len {
     (Array arr length) arr
}

func double_arr (Array (len arr)) -> Array len * 2 {
    ...
}

func requires_array3(Array 3 arr) -> ... {
    ...
}

func init {
    let arr = new_array [1 2 3];
    let new_arr = double_arr arr; // {1, 2, 3, 1, 2, 3}
    
    requires_array3 arr; // works
    requires_array3 new_arr; // ERROR: 'Array 6' is not same type as 'Array 3'
}

With the better example:

func smash (Array (len arr)) (Array (len2 arr2)) -> Array len + len2 {
    ...
}

[TropicSapling]

Other alt. syntaxes:

func (Array a) += (Array b) -> Array c where c length == a length + b length {
    ...
}

// This syntax would require allowing macros to be called inside of function return type
// as well as type pattern matching ('a_len' and 'b_len' can be of any type)
func (Array a_len a) += (Array b_len b) -> Array (a_len + b_len) {
    ...
}