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.

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/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!

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>
  }

The reason for this requirement is lifetime subtyping: 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.

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