John Napiorkowski wrote:
Just curious, how would you feel about an implimentation of dependent types
where the functional element was predefined and more explicit, such as (syntax
hypothetical and only partly implemented...)
<snip>
I am fine with one being able to create, change, and delete the definitions of
data types at runtime, and in fact in the general case of a long-running program
I would expect to be able to do so.
What I expect is that the set of (allowed) member values of a data type is
invariant except by changing the definition of the data type.
And so, a value selector ("object constructor" / "new()") routine, whose
existence and definition automatically falls out of its type's definition (that
is, the act of defining a type also declares that routine), must be a pure
function (that can't invoke 'now'), so that for the entire time that the actual
definition of the type does not change, neither does the set of values / objects
allowed to be selected / constructed of that type.
However, you are free to create or alter or delete the actual data type
definitions themselves as often as you like, and the process of doing that can
of course be dynamic, where runtime-derived values such as the current result of
'now' can be used as a parameter to the definition of the type.
The way I like to think about things is that, while internally the step of
making or changing a type definition, and selecting values of that type, are
internally atomic, they are mutually discrete steps in time.
For example, here are numbered steps in time:
0. No Foo type or Foo values exist.
1. Fetch current datetime and store in $now variable.
2. Declare type Foo (and its selector/constructor) using the value in $now in
its definition.
3. Work with type Foo, selecting and using its values in other variables etc.
4. Fetch current datetime into $now.
5. Alter definition of type Foo using current value of $now.
6. Work with type Foo.
7. Repeat steps 4-6 often as you like.
8. Delete type Foo when done with it.
My key point here is that any impure activity like updating $now with the
current date is done *outside* of either the act of defining or using the Foo type.
Keeping a program defined like this, with separated pure and impure actions,
where the two are associated sequentially in discrete points in time, allows for
cleaner and more deterministic coding. You can effectively have your
DateInThePast type from the perspective of users, but with my proposed design
above, you control exactly when the concept of 'now' changes. The idea here is
that doing it my way will ensure that the concept of 'now' will never vary
within an operation over whose life it is expected to be a constant. And also,
the pure sections can be easier to optimize or memoize because they can safely
assume that things one expects to stay constant will do so, until you explicitly
change them at controlled times. Using 'now' directly everywhere you want to
test for the current date is uncontrolled, especially if you invoke it multiple
times in the same value or constraint expression.
Now, this all said, I think the concept of a DateInThePast type still sounds
rather like a bad program design and should be avoided. While you should be
able to alter types at runtime, there are more practical scenarios where that
would be done, and typically doing so would be infrequent (such as a type
representing a list of valid status codes, or representing the format of what is
considered a well-formed address). But I mentioned DateInThePast as an example
because that is what was used before. In practice one should still just have a
Date type and just have appropriate is-in-past conditionals in the main program
where it actually matters.
-- Darren Duncan
dependent subtype DateBefore($upper_date DateTime),
as $lower_date DateTime,
where {
$lower_date < $upper_date;
};
might be used like (mentally assume a coercion on the date string please):
## ->check($upper_date, $lower_date
DateBefore->check('01-01-2009', '01-01-2000'); ## ok
DateBefore->check('01-01-2009', '01-01-3000'); ## NOT ok
In this case the type is explicitly marked as functional and the requirements
are known upfront and introspectable. I guess the only issue for introspect
and reusability is the fact that the meat of the constraint in in the coderef,
but this could be solved with some sort of type trait mechanism. Consider:
dependent subtype DateBefore($upper_date DateTime),
as $lower_date DateTime,
having isLessThan {
$upper_date;
};
Still very hypothetical syntax but I hope you get the idea. Curious to get
your thoughts (or anyone else's)
