Ok let's try again. We've been working in integrating an small symbolic execution into rustc with @oli_obk. Yesterday we got the compiler to accept the following program: https://play.integer32.com/?version=stable&mode=debug&edition=2018&gist=0428ea00b6d256b70371bcfa06b1783a …
*nods* yeah I've heard that before. But what I'm wondering where the actual limit lies. I'm... not sure now. I guess we don't have any functions that actually operate on types, but are only able to operate on types *inside* the function parameters? At least for now.
-
-
The craziest think that comes to mind is trying to simulate refinement types with this: struct BoolKind<const B: bool>; trait Valid {} impl Valid for BoolKind<true> {} fn first<T, const N: usize>(arr: [T; N]) -> T where BoolKind<{N > 0}>: Valid { arr[0] }
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
I think it's quite limited. We're a long way from being able to express things like fn(x: bool) -> if x { usize } else { isize }
-
In Idris we can write that like this: stringOrInt : Bool -> Type stringOrInt True = Int stringOrInt False = String getStringOrInt : (x : Bool) -> stringOrInt x getStringOrInt x = case x of True => 94 False => "Ninety four"
- 1 more reply
New conversation -
-
-
Most of the things people want from dependent types (ie, theorems!) basically come down to what hinting/proving & solving systems are available, and which parts of the language are available in types! Since rust has (untyped) effects, there's a limit on what can go into a type.
-
Systems like agda/idris/coq/isabelle have a very messy distinction between "representation/storage types" (eg, `i32`) and "proof types" (eg `x >= 3`). I think adding verification support with things lik invariants & refinement types is a better goal than dependent types.
- 8 more replies
New conversation -
-
-
The kinds of pre and postconditions expressible are far more limited with this. You can write all kinds of programs using the rust type system but it would not be a fun experience. Dependent types make many constraints that you have to use asserts for enforcible at compile time.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.