(Idea) Implement built-in Dafny types in Dafny source code

[robin-aws]

Take seq<T> for example. The implementation in the C# and Java runtimes are very similar, and do not simply wrap an existing type in the target language runtime because the lazy evaluation of concatenation is very important for reasonable performance. If this was implemented once in a Dafny prelude instead using classes and traits, and references to seq<T> rewritten in the compiler, we would get several benefits:

1. Formally-verified correctness.
2. No additional per-backend work to support some concepts, unless there was a need to further optimize the default implementation.
3. A mechanism to ensure Dafny contributors "dogfood" the language and implement/maintain non-trivial Dafny code.

This also may apply to some of the types tracked by the Builtins class, such as tuples (which can be thought of as built-in anonymous datatypes).

Related: #1259

[keyboardDrummer]

"If this was implemented once in a Dafny prelude instead using classes and traits, and references to seq rewritten in the compiler"

How come it needs to be defined both in a prelude, and rewritten in the compiler? Are you suggesting to implement Seq in Dafny using arrays and then not having a runtime specific part for it? If so, then what would you need to rewrite in the compiler?

[cpitclaudel]

How come it needs to be defined both in a prelude

I think Robin is suggesting to have a class Seq<T> somewhere and rewrite references from seq<T> to DafnyPrelude.Seq<T>.

It would be nice to be able to just define seq<T> in a regular Dafny file and just include that, though.

[robin-aws]

I just expect this would need at least some compiler rewriting, since you can't just declare seq<T> to be an alias for a reference type in a regular Dafny prelude file. Is IS valid to do that substitution as part of a lowering transformation phase though.

[keyboardDrummer]

Wouldn't the compiler rewrite be to have an implicit opened import of DafnyPrelude, instead of a rewrite specific to seq ?

[robin-aws]

I should not have used the term "prelude" in this case, as I'm not proposing Dafny source code that is directly include-d and import-d, because there isn't a way to declare something like type seq<T> = Sequence<T>.

Sequences are currently implemented in each runtime via one or more target language classes or similar datatypes, such as ISequence<T>, Sequence<T>, ArraySequence<T>, ConcatSequence<T> etc. in C#. I'm only proposing a similar common implementation in Dafny code, which will be compiled to each target language as externs with similar names. Then it is only a matter of tweaking code generation for each language to target the Dafny-generated types instead.

[robin-aws]

This is another improvement for the implementation of sequences that would be much nicer to do once in Dafny rather than N times in each runtime: #2859