proc main(): void {
mut Str[3] v = ["a", "b", "c"]
v = ["x", "y", "z"] // ainda exatamente três: a promessa é mantida
echo v[2] // sem guarda, aqui ou em qualquer lugar
// v = ["x"] // erro de compilação: `v` é declarado Str[3]
}proc main(): void {
mut v := ["a", "b", "c"] // um Str[3]: reatribuído só a três, nunca cresce
v[0] = "x" // escrever através do nome mantém o tamanho
echo v[2]
// v = ["x"] // erro de compilação: `v` é um Str[3]
// v = ["x", "y", "z"] // vale, mas uma reatribuição custa a prova,
// echo v[2] // então isto precisaria de uma guarda
}func twice(n: Int): Int { return n * 2 }
proc main(): void {
Int[2] a = [2, 1]
Int[8] b = [1, 2, 3, 4, 5, 6, 7, 8]
both := a + b // dez elementos: os tamanhos somam
echo both[9] // sem precisar de guarda
doubled := map(a, twice) // ainda dois
ordered := sort(a) // ainda dois
echo "{doubled[1]} {ordered[1]}"
// filter e filterMap não afirmam nada, então seus resultados sempre precisam.
}type Reading {
sectors: Float[3] // três, em toda Reading que existir
notes: Str[dyn] // quantos forem, em cada uma separadamente
}
func slower(was: Reading): Reading {
return Reading([was.sectors[0] + 0.1, was.sectors[1], was.sectors[2]], was.notes)
}
proc main(): void {
mut Reading lap = Reading([31.4, 28.9, 33.2], ["limpa"])
echo lap.sectors[2] // sem guarda: a declaração prometeu três
lap = slower(lap) // um registro inteiramente novo...
echo lap.sectors[2] // ...e ainda três, então ainda sem guarda
// O contrário para um campo [dyn], onde só uma guarda pode dizer:
if lap.notes bounds 0 {
echo lap.notes[0]
}
}Um tamanho estático declarado é uma promessa, e ela é mantida em todo lugar: todo valor que chega em um espaço Str[3] precisa ser um vetor de exatamente três — um inicializador, uma atribuição posterior, um argumento, um campo de um valor construído, um valor retornado — e um tamanho que o compilador não consegue ver também é recusado, e é por isso que split nunca consegue preencher um. Como a promessa vale em todo local de chamada, ela nunca se perde, então um Str[3] pode ser indexado sem guarda mesmo depois de reatribuído, e um parâmetro Str[3] também pode, dentro de quem foi chamado. Um campo é a mesma coisa: um campo Str[3] é exigido em todo lugar onde um valor chega nele, inclusive na construção, então atribuir um registro inteiramente novo o deixa exatamente com três.
Um tamanho inferido é um tamanho do mesmo jeito — mut v := ["a", "b", "c"] só é reatribuído a outro de três e nunca cresce — mas o verificador de limites guarda menos sobre ele. Escrever através do nome mantém a prova; reatribuir o nome a custa, mesmo para o mesmo tamanho, e mesmo dentro de um ramo que pode nem rodar, já que uma prova que só vale às vezes não é uma prova. Declare o tipo quando quiser a promessa, e [dyn] quando quiser um vetor que cresce e vai guardar seus índices.
O que uma guarda prova é mais fraco ainda, e do mesmo jeito: if 2 < len(box.items) trata do valor que o campo guardava naquele instante, então substituir o campo — ou o registro em volta dele — custa a prova, mesmo dentro do ramo que a guarda abriu.
Um tamanho que o compilador conhece sobrevive a tudo que não pode perdê-lo. + soma os dois tamanhos, map mantém o da entrada, e sort também mantém. filter e filterMap não afirmam nada: o que se sabe deles é um máximo, e um máximo nunca coloca um índice na faixa, já que um filtro que não guarda nada é sempre possível.