Comparison of Dependent Types to other languages

Mojo Language Design
1

Background

I started looking at Mojo because this blogpost indicated that it had dependent types. In that blogpost it seemed to jump right to complicated cases without trying something simple. I tried a much simpler case (guessing syntax based on Python).

def test(v: Bool) -> String if v else Int8:
    if v:
        "true"
    else:
        0

and it doesn’t seem to work

error: cannot use a dynamic value in boolean condition
def test(v: Bool) -> String if v else Int8:
                               ^

In something like Lean4 this would work fine:

def test (b: Bool): if b then String else Int :=
  match b with
  | true => "true"
  | false => (0:Int)

This leads me to believe that what mojo is calling dependent types is something else which is more limited in form.

Question

  1. Is there more information about this difference?
  2. Is this a temporary limitation while mojo is in development?
  3. Can someone compare what mojo calls “dependent types” to what theorem provers like Lean call dependent types? For example, does mojo only support type parameters depending on runtime values for their type? Does mojo support Sigma and Pi types?
  4. Does mojo have a way of supporting dependently typed if-then-else?

Extra

The other test case I would normally try for a dependently-typed language is the classic list with type-level length (below in Lean) but it doesn’t seem like mojo has sum/tagged-union/enum types.

inductive Vec (α: Type u) : Nat → Type u where
| nil: Vec α 0
| cons (a:α) (tail:Vec α n): Vec α (n+1)
1 Like
2

Mojo, being a systems-level language, has a restriction that most dependently-typed languages don’t, that all type evaluation has to happen before the program can run. This might make it more accurate to call the type system “a weird cousin of dependent types”. If you were to write code in the parameter domain, for instance a DependentBool[value: Bool] type, you should be able to write the example you proposed once some more type system work is done to handle type refinement. It’s important to note that Mojo’s type system is still a work in progress, so it is more limited than it is planned to be, and that catching up to Rust as far as affine type capabilities are concerned (impl/extension, where/requires, etc) is likely going to take priority over some of the more exotic capabilities of dependent types since people know what those capabilities are and know both that they want them and how to use them.

There isn’t a lot of information about dependent types in Mojo because all most people care about is “better than Rust”. Feel free to ask more questions since a lot of the other language nerds in the community (and at Modular) like to discuss some of the more theoretical aspects of the language. For the most part, all of us have to yield to the practical side and say that dependent types are in service to making the language faster or safer, which means that since the example you have of being able to manipulate the return type of a function using an if statement can be accomplished using function overloading (1), it’s lower priority to make if statements in that position work, since right now there isn’t a unifying type between String and Int in the language since we don’t expose the “type type” in the language yet. This means that the ternary expression, which requires that both brances be the same type, blows up.

There will be ways to, at fairly substantial performance cost, “lift” a runtime type to the parameter domain, but it’s effectively a large switch statement with cases for each value of the type. Unlike other languages with dependent types, it is somewhat accurate to say that Mojo’s will “stop working” once you are done compiling, since Mojo cannot afford the performance penalties that Lean and other “true dependent” languages accept in exchange for that capability. However, if you evaluate that function at compile time instead, yes it should be doable to have that capability. For the most part, I would expect Lean-like capabilities for things which can be fully evaluated at compile time, since we have an interpreter there similar to what Lean has, and things which depend on runtime data will have restricted capabilities. For Sigma and Pi types in particular, I don’t know enough type theory to speak to that, so I’ll tag in @sora .

Yes, Mojo is lacking proper sum types. Everyone working on the language is VERY aware of a desire for this thanks to Rust showing the programming community at large how useful they are. We have Optional, which stores a boolean tag, and Variant, which is a poor man’s sum type that works fine so long as you don’t need 2 names for the same type (ex: 2 named integers). If you need that, you’ll need to newtype so it’s a set of types again.

As for how to implement that extra function in Mojo, you can’t because Mojo will require you to actually build the infinite length List. If you’re fine with a lazy construct then the same tricks as Scala uses, where you capture a closure to generate the nth member of the list or a generator that yields members, will work.

1 Like
3

[…] that all type evaluation has to happen before the program can run.

Ok, that makes sense.

If you were to write code in the parameter domain, for instance a DependentBool[value: Bool] type, you should be able to write the example you proposed once some more type system work is done to handle type refinement.

So, in Lean the test function above is compiled with the result being boxed. Are you saying that in the future this function would work if you did the boxing explicitly with a return type of OwnedPointer[String] if v else OwnedPointer[Int8]?

For Sigma and Pi types in particular, I don’t know enough type theory to speak to that, so I’ll tag in @sora .

:+1:

[…] you can’t because Mojo will require you to actually build the infinite length List.

I’m not sure what infinite list you’re refering to. The Vec is a finite list, it just has the length in the type. You’d use it like this:
#check (Vec.cons 1 (Vec.cons 0 (Vec.nil)) : Vec Nat 2)

I tried something related in mojo below, but it doesn’t seem to work. Is this another instance of the dependent type system still being in-development?

struct Vec[T: ExplicitlyCopyable & Movable, Len: UInt64]:
    var __inner: List[T]

    fn __init__(out self, list: List[T] = []):
        self.__inner = list

    fn push[
        T: Copyable & Movable
    ](self: Vec[T, Len], elem: T) -> Vec[T, Len + 1]:
        var inner2 = self.__inner
        inner2.append(elem)
        return Vec[T, Len + 1](inner2)


def print_only_vec3[T: ExplicitlyCopyable & Movable](x: Vec[T, 3]):
    print("called")


def main():
    var vec0 = Vec[String, 0]()
    var vec1 = vec0.push("1")
    var vec2 = vec1.push("2")
    var vec3 = vec2.push("3")
    # print_only_vec3(vec0)  # doesn't compile, and shouldn't
    # print_only_vec3(vec1)  # doesn't compile, and shouldn't
    # print_only_vec3(vec2)  # doesn't compile, and shouldn't
    print_only_vec3(vec3)  # should compile, but errors

error: invalid call to 'print_only_vec3': argument #0 cannot be converted from 'Vec[String, (((0 + 1) + 1) + 1)]' to 'Vec[String, 3]'
    print_only_vec3(vec3)  # should compile, but errors
    ~~~~~~~~~~~~~~~^~~~~~