Comment by spockz

5 hours ago

If you don’t know at compile time what the type of the value is that is returned, how do you know whether the remainder of the expression is still correct?

The choice is either to have a total function that will be able to deal with every type and check at compile time whether they exist or to defer to the runtime and then throw an exception if the program doesn’t know what to do with the value.

3 comments

spockz

rtpg 10 minutes ago

  getValue : (b : Bool) -> pickType b
  getValue True  = 42
  getValue False = "hello"

So given something like this, imagine something like the following:

  someBool = flipACoinToGetABool
  thingy = getValue someBool

You're already in trouble here right? what's the type of thingy?

So maybe you write:

  thingy: (pickType someBool) = getValue someBool

which is fine and great!

then you write:

  print (thingy + 3) -- thingy can be an int right?

But at this point thingy is of type "pickType someBool" while + is expecting Int. So it's up to you to restructure your code to prove to the type checker that someBool is in fact True.

For example:

   print ((if someBool then thingy else 5) + 3)

^ and here your code proves the fact! So in practice when you want to explore the results that are hidden behind the dependent types, you will need to have written code that unwraps it like this. But the whole point is the underpinning type theory means that you will be fine while doing it! You've proven that it'll be fine, so if you add thingy to 3 you'll have an integer.

I think of this stuff a bit like encryption password. You have this bundle of data, but to get in, you need to provide proof that what you're doing won't blow up. You'll need to write your code in a certain way to do it. But if you provide the right proof, then we're golden.

ChadNauseam 4 hours ago

The value returned by `getValue b` has type `pickType b`. It cannot be used in a way that depends on its type until you check the value of `b`. If `b = True`, then you know that `pickType b = pickType True = Nat` and that therefore `getValue b` has type `Nat`. There is no option to check the type of a value at runtime. You simply cannot use it in such a way as to create a runtime type error. (This is what it means for the types to be erased. The runtime doesn't know what type it's supposed to be!)

skybrian 3 hours ago

Consider how Rust monomorphizes generic functions, making a copy for each possibility. I imagine a compiler could generate a different continuation for each possible return type, along with a runtime check that branches to the appropriate continuation.

It seems like that might cause code bloat, though?