--- On Wed, 4/29/09, Darren Duncan <dar...@darrenduncan.net> wrote:
> From: Darren Duncan <dar...@darrenduncan.net>
> Subject: Re: Types and Constraints
> To: moose@perl.org
> Date: Wednesday, April 29, 2009, 6:01 PM
> Zbigniew Lukasiak wrote [privately]:
> > On Wed, Apr 29, 2009 at 10:28 PM, Darren Duncan <dar...@darrenduncan.net>
> wrote:
> >> Zbigniew Lukasiak wrote:
> >>> It seems that in the Moose terminology a Type
> is just a constraint
> >>> with a name. This is different from
> other languages where the type of
> >>> a value does not change in time or in relation
> to the whole system.
> >>> You can copy the value and be sure that the
> copy has the same type you
> >>> can wait and check the value after some time
> and it's type would not
> >>> change, but if a value type is defined by it
> passing a constraint -
> >>> then these invariants do not hold. For
> example think about a
> >>> constraint that checks if a date is in the
> past.
> >>>
> >>> This is not to criticise this - I understand
> that it is just a
> >>> practical solution - I just want to know if
> there is a consensus that
> >>> it is OK to write Moose types like
> DateInThePast.
> >> In some languages a type is mostly just a named
> set of values, and so it is
> >> valid for the same value to belong to more than
> one type. You see this in
> >> Perl 6 for example; when you define a subtype (eg,
> UInt is subtype of Int
> >> where ...) or a union type (eg, Scalar is union of
> Num|Str etc) values
> >> falling under those still belong to their original
> types but also to the new
> >> ones. That said, even in those cases a value
> would still have just a single
> >> "root type", which is the type whose declaration
> allowed you to select (or
> >> "construct") that value in the first place, and
> any other types would not be
> >> re-introducing the value but just using it. --
> Darren Duncan
> >
> > Hmm - sorry but I don't understand. I
> was writing about the fact
> > that a value at one point can pass a particular
> TypeConstraint - and a
> > second later the same TypeConstraint on the same value
> can fail. This
> > seems to me very different from the way types are used
> in any other
> > language - where if a value is of a particular type
> then it always
> > will. There was nothing about subtypes in my
> question - only about
> > invariants.
>
> Let me clarify, I do believe that all types are / should be
> invariant. I believe that a type system is / should be
> pure and deterministic, and that what values are part of a
> type can not change except by changing the program source
> code that is the type's definition. So anything that
> is impure, including testing what the current date is at
> runtime, can't / shouldn't be allowed in a type
> definition. In other words, there can't / shouldn't be
> a type or TypeConstraint called DateInThePast; rather,
> DateInThePast should be a constraint applied at variable
> assignment time, associated with the variable and not a
> type. The only thing that should be allowable as a
> TypeConstraint like this is, for example,
> DateBefore2009April, and even that is probably a bad design,
> but it is at least pure, and/but I would never do it.
> But better yet, keep the TypeConstraint to just be eg
> "Date", which is invariant. -- Darren Duncan
>
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...)
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)
jnapiorkowski