Dependent types
Bertrand Meyer
I vaguely recall (I did not search the archive) that some time ago someone on this forum asked about the possibility of dependent types for Eiffel. I’d be interested to know if anyone sees a possible application – i.e. examples of things that cannot be done conveniently today and would be cooler with some kind of dependent types (beyond constrained genericity).
Disclaimer: there is no plan to make such major extensions at this point. The focus is entirely on producing the next version of the Ecma standard (which is progressing – this in case you wonder). Asking purely from a perspective of intellectual curiosity.
-- BM
Miguel Oliveira e Silva
Although I don't do much functional programming -- and if I understand dependent types correctly --, enriching the static type system with this possibility might indeed ensure some very interesting invariants at compile time [1]. For instance: statically ensure a fixed size for an array (to represent a 2D, or 3D vector, or correct matrix operations). If such possibility is feasible (and not to awkward for programmers), it could be a very interesting addition. It surely could make a positive contribution to the ultimate goal of statically ensured correctness (as much as possible) and to enhance code reuse (in the example given, to avoid the more conservative approach of defining a VECTOR_2D, and VECTOR_3D classes).
In my view, to achieve such goal in an OO programming language the key is -- again [2] -- object construction/creation. Perhaps link type values to read-only immutable attributes (similar to Current), whose value can be ascertain at compile time (better yet, ascertain a value predicate enough to ensure static safety).
In attachment follows a very rudimentar (and incomplete) first example to such a possibility (with some Eiffel alike syntactical approaches).
Best regards,
-miguel
[1] Even if not using the full expressive power of functional dependent types.
[2] As, in my view, they are for n-ary dynamic dispatch (https://sweet.ua.pt/mos/external-dispatch-eiffel/index.html)
--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/263701dc623f%2405d418c0%24117c4a40%24%40inf.ethz.ch.
-- Miguel Oliveira e Silva IEETA-DETI, University of Aveiro, Portugal
Ulrich Windl
If your focus is on the fixed size, couldn't you derive from ARRAY, adding assertions about the size (when creating)?
If your focus is on efficiency, wouldn't it be a kind of "expanded ARRAY" (fixed size)?
I also wondered: if a generic type declaration would not only allow types, but also (natural?) integers, couldn't you use such mechanism to declare fixed size ARRAYs? Like "a: VECTOR[INTEGER, 2]".
Ulrich
02.12.2025 15:30:33 Miguel Oliveira e Silva <m...@ua.pt>:
>>
Miguel Oliveira e Silva
Hi Ulrich,
I'm not advocating the necessity for dependent types (DP) in Eiffel (in fact, up to two days ago, I don't think I ever thought about it). I'm just following Bertrand's challenge for possible DP applications, and thinking (crudely) on its implications on the language and how it could be expressed. It seems an interesting language extension to, at least, think more profoundly about it (and a much more profound analysis than mine is definitely required).
If I understand correctly DT, the difference to (normal DbC) assertions is that it is part of the type system, and it is 100% ensured at compile time: All the computations involved in DT is done statically by the compiler type system. DT enable the possibility to use values, and value expressions, as part of a type definition (resulting in a much more complex type system).
I think that the focus for DT is (static) correctness and also reuse (no need to create extra classes just to ensure some invariants, such as a 3D vector). Efficiency could also be a positive side-effect because all type computations are done at compile time.
Using class generics to express dependent types is a very interesting and, at first sight, coherent syntactical alternative.
DP should not be restricted to integers or natural numbers [1]. In attachment follows another (crude) example using strings in a DT definition, this time, just for fun, using a syntactical alternative based on generic classes.
-miguel
[1] It should apply to any value, and value expression (and lambda expressions?), that can be completely resolved at compile time.
-- You received this message because you are subscribed to the Google Groups "Eiffel Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/dd99bf34-f067-497a-8808-0693b144ece1%40gmail.com.
Woland's Cat
- based on String: types like Uri, Urn, Uid, and any privately created type representing identifiers with specific syntax, typically given by a regex
- based on a type we call Terminology_code, we create pseudo-types like: 'language : Terminology_code «iso.iso_639-1»', where the '«iso.iso_639-1»' limits the range. These are not real types, but something more like a type with a limited range. A 'Terminology code' is a code e.g. 'en' from a terminology that is named, e.g. ISO 639-1.
- based on String and Integer, we create Enumeration types, which look as below.
enumeration Sample_function_kind
base_type String
feature_group ("values")
actual ("actual");
minimum ("minimum");
maximum ("maximum");
mean ("mean");
mode ("mode");
median ("median");
increase ("increase");
decrease ("decrease");
change ("change");
total ("total");
end
--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/263701dc623f%2405d418c0%24117c4a40%24%40inf.ethz.ch.