Function parameters of arrays sized m, n → m+n is the hello world of dependent types. I hacked this together over two evenings:

use 5.038; use strictures; use Kavorka qw(fun); use Moops; our %TypeVarRegistry; class MyTypes extends Type::Library :ro { use Type::Library -declare => qw(TypeVar TypeVarExpr); use Types::Common::String qw(NonEmptyStr); use Types::Standard qw(ArrayRef); use Types::Common::Numeric qw(PositiveOrZeroInt); my $TypeVar = Type::Tiny->new( name => 'TypeVar', constraint_generator => fun(NonEmptyStr $name → CodeRef) { fun {} } ); my $TypeVarExpr = Type::Tiny->new( name => 'TypeVarExpr', constraint_generator => fun(NonEmptyStr $name → CodeRef) { fun {} } ); my $SizedArray = Type::Tiny->new( name => 'SizedArray', parent => ArrayRef, constraint_generator => fun( Enum["type"] $literal_type, Type::Tiny $parameterized, Enum["length"] $literal_length, $expr → CodeRef ) { if (PositiveOrZeroInt->check($expr)) { fun { $expr == ArrayRef->of($parameterized)->assert_return($_)->@* } } elsif ('TypeVar' eq $expr->parent->name) { fun { $TypeVarRegistry{$expr->parameters->[0]} = ArrayRef->of($parameterized)->assert_return($_)->@*; 1 } } elsif ('TypeVarExpr' eq $expr->parent->name) { fun { my $eval; # world's worst symbolic expr parser if ( my ($var1, $op, $var2) = $expr->parameters->[0] =~ /(\w+)(\+)(\w+)/ ) { $eval = $TypeVarRegistry{$var1} + $TypeVarRegistry{$var2}; } else { die; } $eval == ArrayRef->of($parameterized)->assert_return($_)->@* } } else { die } }, ); __PACKAGE__->meta->add_type($_) for $TypeVar, $TypeVarExpr, $SizedArray; __PACKAGE__->meta->make_immutable; } use MyTypes qw(SizedArray TypeVar TypeVarExpr); fun add_ok( SizedArray[type => Str, length => TypeVar["m"]] $A, SizedArray[type => Str, length => TypeVar["n"]] $B → SizedArray[type => Str, length => TypeVarExpr["m+n"]] ) { [$A->@*, $B->@*] } use Data::Dx; Dx add_ok([qw(e r t)], [qw(e r t)]); fun add_broken( SizedArray[type => Str, length => TypeVar["m"]] $A, SizedArray[type => Str, length => TypeVar["n"]] $B → SizedArray[type => Str, length => TypeVarExpr["m+n"]] ) { [$A->@*, $B->@*, 'this must not work'] } use Data::Dx; Dx add_broken([qw(a s d f)], [qw(g h j k)]); 

submitted by /u/daxim
[link] [comments]