Type system questions.

5 views
Skip to first unread message

Autrijus Tang

unread,
May 3, 2005, 5:06:15 AM5/3/05
to perl6-l...@perl.org
With the recent discussion on type sigils, and the fact that Pugs
is moving toward the OO core, I'd like to inquire how the following
statements evaluate (or not):

# Compile time type arithmetic?
::Dual ::= ::Str | ::Num;
$*Dual ::= ::Str | ::Num;

# Run time type arithmetic?
my ::dual := ::Str | ::Num;

# Type Instantiation?
sub apply (&fun<::a> returns ::b, ::a $arg) returns ::b {
&fun($arg);
}

# Does Role live in the same namespace as Types/Classes/Modules/Packages?
my ::role = role { ... };

# Can class take type parameters like Roles cna?
class Pet[Type $petfood] {
method feed (::($petfood) $food) {...}
}

# Single colon as tuple composer?
my $Triple ::= :(Bool, Int, Str);
my $TripleTuple ::= :($Triple, $Triple);
my &pair_with_int ::= -> Type ::t { :(::t, Int) };

Thanks,
/Autrijus/

Larry Wall

unread,
May 3, 2005, 8:32:44 AM5/3/05
to perl6-l...@perl.org
On Tue, May 03, 2005 at 05:06:15PM +0800, Autrijus Tang wrote:
: With the recent discussion on type sigils, and the fact that Pugs

: is moving toward the OO core, I'd like to inquire how the following
: statements evaluate (or not):
:
: # Compile time type arithmetic?
: ::Dual ::= ::Str | ::Num;

Yes, but I think that is the same as

our ::Dual ::= ::Str | ::Num;

which sets Dual in the current package, not in *.

Also, the :: is of course optional on the existing types.

: $*Dual ::= ::Str | ::Num;

Probably works, assuming types autoenreference in scalar context so that

$*Single ::= Str;

is equivalent to

$*Single ::= \Str;

: # Run time type arithmetic?


: my ::dual := ::Str | ::Num;

Yes.

: # Type Instantiation?


: sub apply (&fun<::a> returns ::b, ::a $arg) returns ::b {
: &fun($arg);

: }

The first parameter would be &fun:(::a) these days, but yes.
(Stylistically, I'd leave the & off the call.)

: # Does Role live in the same namespace as Types/Classes/Modules/Packages?


: my ::role = role { ... };

Yes, though in this case that namespace is a subset of the lexical
namespace.

: # Can class take type parameters like Roles cna?


: class Pet[Type $petfood] {
: method feed (::($petfood) $food) {...}

: }

Don't think so. I'd like to keep generics/parametric types associated
with roles if possible, so that we know exactly when they are composed
into a class. If that means we have to write a few classes that do
nothing but wrap around a role, I think it's probably worth it.

: # Single colon as tuple composer?


: my $Triple ::= :(Bool, Int, Str);
: my $TripleTuple ::= :($Triple, $Triple);
: my &pair_with_int ::= -> Type ::t { :(::t, Int) };

I think of it as the signature composer. Does Haskell call them
tuples? That word tends to mean any immutable list in other circles,
though I suppose :(4, 2, "foo") could be construed as a type whose
values are constrained to single values. But it makes :(int $x)
terribly ambiguous if it's an evaluative context. (Which is why
we wanted :() in the first place, to avoid such evaluation.)

Larry

Autrijus Tang

unread,
May 3, 2005, 9:53:59 AM5/3/05
to perl6-l...@perl.org
On Tue, May 03, 2005 at 05:32:44AM -0700, Larry Wall wrote:
> : # Type Instantiation?
> : sub apply (&fun<::a> returns ::b, ::a $arg) returns ::b {
> : &fun($arg);
> : }
>
> The first parameter would be &fun:(::a) these days, but yes.
> (Stylistically, I'd leave the & off the call.)

So, the "returns" trait is not part of a function's long name, but
it can still be matched against (and instantiated)?

Hrm, is it specific to the "returns" trait, or we can match against
any traits at all?

sub foo ($thingy does Pet[::food]) { ... }

Also, S12 talks about "is context":

method wag (*@args is context(Lazy)) { $:tail.wag(*@args) }

What is the type of "Lazy" here? Also, is "context" a role or a class?
If it is a class, how does it parameterize over "Lazy" ?

> : # Single colon as tuple composer?
> : my $Triple ::= :(Bool, Int, Str);
> : my $TripleTuple ::= :($Triple, $Triple);
> : my &pair_with_int ::= -> Type ::t { :(::t, Int) };
>
> I think of it as the signature composer. Does Haskell call them
> tuples? That word tends to mean any immutable list in other circles,
> though I suppose :(4, 2, "foo") could be construed as a type whose
> values are constrained to single values.

Err, sorry, I meant "tuple type composer". In haskell:

-- Value -- -- Type --
(True, 1, "Hello") :: (Bool, Int, Str)

This was because I couldn't think of other operators other than ","
to operate on types inside :(). Come to think of it, there are lots
of other things possible:

my $SomeType ::= :((rand > 0.5) ?? Bool :: Int);

Also, is it correct that (4, 2) can be typed as both a :(Eager) list and a
:(Any, Any) tuple? Is it generally the case that we can freely typecast
unbounded list of values from (and to) bounded ones?

> But it makes :(int $x) terribly ambiguous if it's an evaluative
> context. (Which is why we wanted :() in the first place, to avoid
> such evaluation.)

Evaluative context?

However, I'm a bit confused now. Does a :(...) expression stand for a
type, a variable binding, or both?

:($x) # variable binding or deref $x into a type?
:(Int) # a type?
:(Int $x) # bind a type into $x?

If all three are allowed, then :($x) itself is ambiguous... What would
these mean, then?

:(:(Int $x) | :(Str $y));
:((Int $x) | (Str $y));

Thanks,
/Autrijus/

Thomas Sandlaß

unread,
May 3, 2005, 12:40:39 PM5/3/05
to perl6-l...@perl.org
Autrijus Tang wrote:
> On Tue, May 03, 2005 at 05:32:44AM -0700, Larry Wall wrote:
>
>>: # Type Instantiation?
>>: sub apply (&fun<::a> returns ::b, ::a $arg) returns ::b {
>>: &fun($arg);
>>: }
>>
>>The first parameter would be &fun:(::a) these days, but yes.
>>(Stylistically, I'd leave the & off the call.)

I am still advocating for :() beeing the type sublanguage.
But I'm not sure if @Larry are already that far ;)
Why not &fun:( ::a returns ::b )?


> So, the "returns" trait is not part of a function's long name, but
> it can still be matched against (and instantiated)?

The long name of a function consists of three parts:

1) the invocant type list
2) the parameter type list
3) the return type list

like &code:( Int, Dog : Str returns Bool ). Actually the ?+*
markers should be in there, too. Nesting should work as well,
but might not need the colon?


> Hrm, is it specific to the "returns" trait, or we can match against
> any traits at all?

Well, I think everything that is part of the type language/system
should go into :(). That IMHO includes does, where and ranges.


> This was because I couldn't think of other operators other than ","
> to operate on types inside :(). Come to think of it, there are lots
> of other things possible:
>
> my $SomeType ::= :((rand > 0.5) ?? Bool :: Int);

I guess this drives the typechecker to the brink of madness---or beyond.
OTOH, junctive types in the sense of glb and lub would be fine in my mind!


> Also, is it correct that (4, 2) can be typed as both a :(Eager) list and a
> :(Any, Any) tuple? Is it generally the case that we can freely typecast
> unbounded list of values from (and to) bounded ones?

Uho, big can of (type)worms! First of all we might run into the co-/contra-variance
issue of parametric types. Secondly it should work only one way. The other way
round would be a type error unless tuple and list are equal types. The usual type
theoretic definition of subtyping on tuples is to demand that the subtype relation
holds pairwise. But note that type theory doesn't really handle imperative features
very well.


>>But it makes :(int $x) terribly ambiguous if it's an evaluative
>>context. (Which is why we wanted :() in the first place, to avoid
>>such evaluation.)

Ups, I would hope we only have type variables inside of :() expressions,
that is ones prefixed with the :: type sigil. And I would like to see a
constraint language. So that e.g. the classical "feed the animal" method
type can be specified generically:

subtype &eat:( ::a does Animal : does Food of ::a ) of Method;
invocant : parameter

I'm not sure if that syntax is supported, though.

Such a method should be callable on all objects that
1) do the Animal role
2) for which a class exists that does the corresponding Food role

Or more concrete:

class Cow does Animal {...}
class Grass does Food of Cow {...}
class Meat does Food of ::Tiger {...}

sub foo ( Cow $elsa, Grass $green, Meat $raw )
{
$elsa.eat( $green ); # OK
$elsa.eat( $raw ); # error
$_.eat( $raw ); # works if $_.does( Tiger )
}

The above errors might be detectable at compile time,
but not these:

sub bar ( Animal $elsa, Food $green, Food $raw )
{
$elsa.eat( $green );
$elsa.eat( $raw );
}

not to mention something vague like

sub baz ( $x, $y )
{
$x.eat( $y );
.eat; # topic eats itself? Sorry, couldn't resist.
}

Also note that &bar is not necessarily a subtype of &foo because it
depends on Food[Cow] and Food[Tiger] beeing subtypes of Food, while
Cow is a subtype of Animal.

But it might be only me striving for CBP (Constraint Bounded Polymorphism).
YMMV :)
--
TSa (Thomas Sandlaß)

Larry Wall

unread,
May 4, 2005, 3:56:09 PM5/4/05
to perl6-l...@perl.org
On Tue, May 03, 2005 at 09:53:59PM +0800, Autrijus Tang wrote:

: On Tue, May 03, 2005 at 05:32:44AM -0700, Larry Wall wrote:
: > : # Type Instantiation?
: > : sub apply (&fun<::a> returns ::b, ::a $arg) returns ::b {
: > : &fun($arg);
: > : }
: >
: > The first parameter would be &fun:(::a) these days, but yes.
: > (Stylistically, I'd leave the & off the call.)
:
: So, the "returns" trait is not part of a function's long name, but
: it can still be matched against (and instantiated)?

Well, we've made some rumblings about the return type being a
tiebreaker on MMD after all other invocants have been considered,
but other than that, I don't consider it a part of the long name,
at least for standard Perl 6 as currently defined. An MLish version
of Perl might. But maybe installing the return type inside the
signature is a way to indicate that you want the return type considered.

: Hrm, is it specific to the "returns" trait, or we can match against

: any traits at all?
:
: sub foo ($thingy does Pet[::food]) { ... }

Which is basically what

sub foo (Pet[::food] $thingy) { ... }

is doing already, unless you consider that what $thingy returns is
different from what it actually is, which would be odd.

: Also, S12 talks about "is context":


:
: method wag (*@args is context(Lazy)) { $:tail.wag(*@args) }

That is probably misspecified slightly, insofar as the context is
already lazy by default. The problem is that the incoming Lazy
is being bound as the .specs of an Array, and I was thinking the
flattening aspects of an array might cause a double flattening
when we pass it on to the delegated method. But I suppose if we
work it right, a simple

method wag (*@args) { $:tail.wag(*@args) }

should coalesce the two abstract flattenings of the two calls into one
actual lazy flattening.

: What is the type of "Lazy" here?

Intended to be an ordinary lazy list such as you always get in for
the list unless you force it to be eager. It basically is what is
bound to the .specs of the Array for its generators, if I'm thinking
about it right.

: Also, is "context" a role or a class?

I'd call it a trait in this case since it's apparently doing heavy duty
context magic to the parse (which you can't do with a method anyway...)

: If it is a class, how does it parameterize over "Lazy" ?

It's mostly there to allow "is context(Scalar)" so we can have
a subroutine call with a list of scalars. But we also want "is
context(Eager)" functionality to force eager flattening of the list.
The latter currently has a shorthand of

sub foo (**@_) {...}

to get a P5 style immediate flattening.

: > : # Single colon as tuple composer?


: > : my $Triple ::= :(Bool, Int, Str);
: > : my $TripleTuple ::= :($Triple, $Triple);
: > : my &pair_with_int ::= -> Type ::t { :(::t, Int) };
: >
: > I think of it as the signature composer. Does Haskell call them
: > tuples? That word tends to mean any immutable list in other circles,
: > though I suppose :(4, 2, "foo") could be construed as a type whose
: > values are constrained to single values.
:
: Err, sorry, I meant "tuple type composer". In haskell:
:
: -- Value -- -- Type --
: (True, 1, "Hello") :: (Bool, Int, Str)
:
: This was because I couldn't think of other operators other than ","
: to operate on types inside :(). Come to think of it, there are lots
: of other things possible:
:
: my $SomeType ::= :((rand > 0.5) ?? Bool :: Int);

I don't think that amount of generality should be allowed in :(), at least,
not without something explicitly interpolative, like

my $SomeType ::= :( ::( (rand > 0.5) ?? Bool :: Int ) );

: Also, is it correct that (4, 2) can be typed as both a :(Eager) list and a


: :(Any, Any) tuple? Is it generally the case that we can freely typecast
: unbounded list of values from (and to) bounded ones?

I don't offhand know what restrictions we might want to put on it.

: > But it makes :(int $x) terribly ambiguous if it's an evaluative


: > context. (Which is why we wanted :() in the first place, to avoid
: > such evaluation.)
:
: Evaluative context?
:
: However, I'm a bit confused now. Does a :(...) expression stand for a
: type, a variable binding, or both?
:
: :($x) # variable binding or deref $x into a type?
: :(Int) # a type?
: :(Int $x) # bind a type into $x?

I was thinking of it only as signature syntax, so it would always be
a variable binding, or pseudo-binding where it doesn't make sense to
actually create a variable. I was thinking that the syntax might even
just allow you to drop the identifier, so :($:?%,*@) is a valid type,
identical to :($x: ?%y, *@z) when the names don't matter.

By the way, the problem with just throwing a "returns" in the sig is
that

:($x: ?%y, *@z returns Int)

would be taken as

:($x: ?%y, Int *@z)

So maybe it would have to be written

:($x: ?%y, *@z, :returns(Int))

or maybe something like

:($x: ?%y, *@z --> Int)
:($x: ?%y, *@z ==> Int)
:($x: ?%y, *@z >> Int)
:($x: ?%y, *@z » Int)

which suggests we could have return types on pointy subs:

$result = do given foo() -> $x --> Int { $x // $default }
$result = do given foo() -> $x ==> Int { $x // $default }
$result = do given foo() -> $x >> Int { $x // $default }
$result = do given foo() -> $x » Int { $x // $default }

and expect $result to contain the integer value of either $x or $default.
But we can solve that another day.

: If all three are allowed, then :($x) itself is ambiguous... What would


: these mean, then?
:
: :(:(Int $x) | :(Str $y));
: :((Int $x) | (Str $y));

I expect we can probably disallow or ignore the use of variable names
where nonsensical.

Larry

Reply all
Reply to author
Forward
0 new messages