5 ms·

This is one of my favorite patterns from Haskell, which I've known as "type-level programming". One of the most common examples is a "sized vector"[1] which all

This is one of my favorite patterns from Haskell, which I've known as "type-level programming". One of the most common examples is a "sized vector"[1] which allows compile-time bounds checking. This is achieved by annotating each vector type with a phantom type variable representing its size. Nice to see something like this in Rust! One thing that's a bit of a bummer, and I'm sure there are very good reasons for this, is that we HAVE to use every type argument of struct in its definition. If this restriction were to be relaxed, we wouldn't need the "state" field in the struct at all, and we could make the state type variable truly "phantom". [1] https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell https://www.schoolofhaskell.com/user/konn/prove-your-haskell... EDIT: Typos.

choudanu4 7y ago
Does the PhantomData type in Rust do what you want? Or are you talking about something slightly different? https://doc.rust-lang.org/nomicon/phantom-data.html https://doc.rust-lang.org/nomicon/phantom-data.html https://doc.rust-lang.org/std/marker/struct.PhantomData.html https://doc.rust-lang.org/std/marker/struct.PhantomData.html So struct Sender<S> { /// Actual implementation of network I/O. inner: SenderImpl; /// 0-sized field, doesn't exist at runtime. state: S; } I believe could become struct Sender<S> { /// Actual implementation of network I/O. inner: SenderImpl; /// 0-sized field, doesn't exist at runtime. _marker: PhantomData<S>; } I've never used this PhantomData personally, so this might be wrong. Cheers!
- dmkolobov 7y ago
  It does! But you still have to actually "use" it, meaning that it appears as a field in the definition, and you have pass a PhantomData value whenever you create new instances of your data type. In Haskell, you can omit these fields entirely, and achieve the same thing just by annotating the function. For example, in Haskell, we can have data Const a b = Const a whereas in Rust, it would be: struct Const<A, B> { konst: A, // does not exist at run-time discard: PhantomData<B> }
  - Rusky 7y ago
    The reason for this requirement is lifetime subtyping: https://doc.rust-lang.org/nomicon/subtyping.html https://doc.rust-lang.org/nomicon/subtyping.html Type parameter variance is inferred from usage (e.g. covariant for normal fields, contravariant for function arguments) and without a usage there's no way to infer it.
kccqzy 7y ago
No. Singletons in Haskell are the single most over-engineered and ugliest thing I've seen. If you are going this route, you might as well use a real dependently typed language like Agda or Coq, and the latter supports extracting simple Haskell code from your Coq code while keeping your proofs in Coq. Indexed types have their uses but just think about this: for your length-indexed vector example, what if you want to read a file and put its lines into such a vector? Your return type needs the length but it's not known until runtime. Okay you use existential quantification, but you now also need a runtime representation of your types. That's done through singletons. But that destroys Haskell's phase separation and means the inefficient ways you use to prove things and encode naturals now leak to the runtime! Have fun with your unary numbers then.
likeliv 7y ago
There is an example of indexed vecteur in the rustc source code https://github.com/rust-lang/rust/blob/master/src/librustc_index/vec.rs https://github.com/rust-lang/rust/blob/master/src/librustc_i...

choudanu4 7y ago

Does the PhantomData type in Rust do what you want? Or are you talking about something slightly different? https://doc.rust-lang.org/nomicon/phantom-data.html https://doc.rust-lang.org/nomicon/phantom-data.html https://doc.rust-lang.org/std/marker/struct.PhantomData.html https://doc.rust-lang.org/std/marker/struct.PhantomData.html So struct Sender<S> { /// Actual implementation of network I/O. inner: SenderImpl; /// 0-sized field, doesn't exist at runtime. state: S; } I believe could become struct Sender<S> { /// Actual implementation of network I/O. inner: SenderImpl; /// 0-sized field, doesn't exist at runtime. _marker: PhantomData<S>; } I've never used this PhantomData personally, so this might be wrong. Cheers!

dmkolobov 7y ago
It does! But you still have to actually "use" it, meaning that it appears as a field in the definition, and you have pass a PhantomData value whenever you create new instances of your data type. In Haskell, you can omit these fields entirely, and achieve the same thing just by annotating the function. For example, in Haskell, we can have data Const a b = Const a whereas in Rust, it would be: struct Const<A, B> { konst: A, // does not exist at run-time discard: PhantomData<B> }
- Rusky 7y ago
  The reason for this requirement is lifetime subtyping: https://doc.rust-lang.org/nomicon/subtyping.html https://doc.rust-lang.org/nomicon/subtyping.html Type parameter variance is inferred from usage (e.g. covariant for normal fields, contravariant for function arguments) and without a usage there's no way to infer it.

kccqzy 7y ago

No. Singletons in Haskell are the single most over-engineered and ugliest thing I've seen. If you are going this route, you might as well use a real dependently typed language like Agda or Coq, and the latter supports extracting simple Haskell code from your Coq code while keeping your proofs in Coq. Indexed types have their uses but just think about this: for your length-indexed vector example, what if you want to read a file and put its lines into such a vector? Your return type needs the length but it's not known until runtime. Okay you use existential quantification, but you now also need a runtime representation of your types. That's done through singletons. But that destroys Haskell's phase separation and means the inefficient ways you use to prove things and encode naturals now leak to the runtime! Have fun with your unary numbers then.

likeliv 7y ago

There is an example of indexed vecteur in the rustc source code https://github.com/rust-lang/rust/blob/master/src/librustc_index/vec.rs https://github.com/rust-lang/rust/blob/master/src/librustc_i...