On Thu, Apr 30, 2009 at 12:15 AM, Stevan Little
<stevan.lit...@iinteractive.com> wrote:
>> I was not talking here about variables (where the 'statically typed'
>> term could be applied) I was talking about values.
>
> Okay, I am kind of confused then.
>
> If "foo" is a value whose type is a string, then (aside from the automatic
> coercion into a number) Perl does this already.
>
> Taking it one step further, {} is a value whose type is a hash. I can mutate
> the hash, but does that change it's intrinsic type? It is still a hash isn't
> it?
>
> When I am speaking about variables, I am taking about "containers". Where $x
> is a container that can hold a SCALAR value. Same goes for %x, which is a
> container that can hold a hash. The value's inside these containers can be
> changed, but $x will still just hold a SCALAR and %x will still just hold a
> HASH. Different values, but same containers.
>
> This is why some people say perl is strongly typed, because $x will always
> only hold a SCALAR, @x an ARRAY and %x a HASH. I tend to not agree with this
> fact because all of perl's automatic coercion (my $x = @x, etc) means that
> these "strong" types are not al that strong.
>
> In my mind (CAVEAT: I am not a computer scientist or a professional type
> theorist and I *fully* admit that the deeper parts of type theory go *way*
> above my head, I am speaking on my (possibly wrong, possibly right, probably
> somewhere in between) understanding of things only), having types on values
> is not terribly useful. 1 will be 1 always, it won't change. Same is true of
> (1, 2, 3), it will always be the same value (you can't mutate it until you
> assign it into a variable). These are literal values and their type will
> never change because they are constant values.
>
> Now, variables/containers are where it gets more interesting. But it is 6pm
> EST and I am too hungry to dive into some long rant about type stuff.
>
> So, perhaps I am not understanding your use of "values" here. Can you
> elaborate?Sure - lets say a data type is the set of values allowed in some place of the computer program. When I say type of a value I have in mind the set that this value belongs to. Of course a value can belong to more than one set (say Integer and Real numbers). In that formalism a subtype is subset - as Darren explained already. Now the important point of that definition is that this set is defined once and forever - it does not change with the execution of the program or other circumstances - and a value can belong to it or not but it cannot belong to it at some point and later not. So if we take 29th of April 2009 - it belongs to the set of dates < 30th of April 2009 - and that can be a type in this formalism, but dates < now() is not a set - it is a function that takes a point in time and returns a set. And that brings us to the 'dependent types' - I don't really know this term - but intuitively it does fit here - DateInThePast could be called a dependent type, as it is a set of dates that depends on what is current point in time. As a disgression - I've also talked to John about his implementation of dependent types - and I think what he has in mind is slightly different - it is more about 'parametrized types'. As I argument above dependent types are already there in Moose. ... > >> Now take DateInThePast - the same value (lets say 29th of April 2009) >> can at one point have that type and at another point in time it will >> not have that type. > > Yes, okay, so this is a fine line and not really the best example because > unless you have a time machine the 29th of April 2009 will always be a date > in the past (well technically not until tomorrow, but you get the point). > > This is getting into (my understanding of) the world of dependent types. > This is types where the actual value is relevant to the type definition and > not just the "type" of the value. In this case DateInThePast is of the type > Date, but it's value (a date in the past) is what you are more interest in. > > Dependent types are pretty nutty things and I only just sorta feel like I > understand then, but not quite. I have seen some arguments that basically > declare them useless since to properly dependently type check a program you > could have execute the entire thing at compile time (how else would you know > the values themselves, not just their types). > My point is that with the current implementation nothing prevents you from defining a type like DateInThePast - you just need to use a localtime call in the constraint. So you can define dependent types - and my question was is there a consensus that this is OK to use that possibility? I mean dependent types are something rather different from the standard types - so it can be surprising for someone coming from a different background. And - this is really just an aside - and also I don't really know the theory behind 'dependent types' - but it all seems to me that calling all of it just Constraints would be more consistent with the general intuition (with subconstraints - maybe not immediately obvious that it would mean a more restrictive constraint - but not that bad). > Anyway again, too hungry for heavy type theory and I am not really a good > resource here anyway. > >> The point is that in the Moose type system these sentences don't have >> any meaning at all - because it is not the value that has the type. > > Okay, so yeah sure. This is why it is a "type constraint" system. But again > I don't really get what is so interesting about knowing that 1 is a type > Number, I think it is more useful to know that given $x = 1, $x is currently > holding a value which is of type Number and through that $x is (sorta) of > the type Number. > My point is about what you are using the types for - and the standard answer is that that they answer if you can use a given value/variable in a given place in the program. But if you allow types like DateInTheFuture (dependent types?) - then if you check a value at one point in the program - you don't know if you can use that value at another point in it - because in the meantime it can become a DateInThePast. I understand that for most usage this is just splitting hairs. -- Zbigniew Lukasiak http://brudnopis.blogspot.com/ http://perlalchemy.blogspot.com/
