Mudanças no Compiler

ata.md

Mudanças e ideias para o Kind2

Algumas mudanças bem importantes na linguagem vão ocorrer pelos próximos dias e que vão influenciar bastante o modo que programamos Kind2. Primeiro eu gostaria de introduzir as ideias que a linguagem tenta usar e, após isso, os problemas que pensei que não vão deixar a linguagem ir tanto para frente quanto eu queria.

Ideais

A unidade de modularização da linguagem seriam as funções já que tudo em Kind é primordialmente uma função ou um construtor (você pode considerar os 2 a mesma coisa já que um construtor é uma função que não reduz) e isso molda varios aspectos da linguagem como:

• Arquivos: Na maioria das vezes um arquivo contém uma função "publica" quer teria o nome igual ao seu path relativo ao em que você ta executando o Kind trocando por "/" por "." e removendo o ".kind2".
• Share: A forma de compartilhar código seria por publicação de funções individuais com nomes únicos globalmente. Isso faz sentido para definições puramente matemáticas como um Monoid ou Semigroup que, apesar de existirem formas diferentes de definir a mesma coisa, ainda tem uma estrutura bem definida.

Problemas com funções com nomes "universais"

Tudo seria função, sem arquivo de configurações, boilerplates ou arquivos desnecessários. Escreva kind2 check bla.kind2 e seja feliz. Apesar dessas ideias serem bem legais, eu não vejo sendo bem realistas. Nenhum nome pode descrever precisamente muitos algoritmos que variam muito. No caso de termos um functions.kindelia.org, alguém teria que ficar moderando os publishments para ver se realmente o nome bate com o que o algoritmo faz. Não haveria updates destrutivos de uma função que pode estar bugada porque isso provavelmente quebraria todos os códigos existentes. Caso a gente prefira versionar as funções, iriamos ter um INFERNO NA TERRA com erros como Type mismatch: expected: List.1.0.0 but instead got List.1.0.1 quando você tenta usar duas funções que usam versões diferentes da mesma função.

Problemas com os nomes como são hoje

Funções devem começar com letras maiúsculas e o compilador não ta forçando isso por enquanto. Um exemplo é definir a função ata e receber esse erro bem feio na sua cara.

Unbound variable: `ata.`.
On rule: `(Q$ata orig) = (Kind.Term.fn0 ata. orig)`.

Outro problema é relativo a todas aplicações de função precisarem ser em uma linha só (caso não tenha parenteses) Que para o código:

ata : U60
ata = 
    a
    b

be : U60
be = 2

Gera esse erro deprimente:

[teste.kind2]
Expected `<`:
  6 | be : U60

Esses problemas vão ser consertados, mas pequenos aspectos da sintaxe da linguagem vão mudar, deixando mais específico como que as expressões são compostas. Provavelmente eu vou colocar todas essas mudanças no CHANGELOG mas tenha conciencia de que alguns pedaços pequenos de sintaxe não vão mais serem aceitos.

Encurtamento de nomes

Hoje em dia existem funções com nomes ENORMES como:

Algebra.Monoid.identity <t> (monoid: Algebra.Monoid t): Algebra.Laws.Identity t (Algebra.Monoid.concat monoid) (Algebra.Monoid.empty monoid)
Algebra.Monoid.identity t (Algebra.Monoid.new t_ sg empty id) = id

Há uma proposta de como relativizar nomes mas o design não está fechado. As regras seriam:

• Caso o nome comece com / como /identity, ele se refere ao namespace atual. Então se eu estou em Algebra/Monoid/identity.kind2 e eu escrevo /pudim, estou me referindo a Algebra/Monoid/pudim.kind2.
• Caso eu tenha um use Algebra.Monoid as M no topo do meu arquivo, eu posso usar M/seila para encurtar esse nome. Caso eu não coloque um nome após como M/ ele irá remover o . e irá ficar M.

Um problema que pode surgir com M/ é que se eu coloco algo após ele como M/ U60, fica difícil de perceber se é M/U60 (Algebra.Monoid.U60) ou M/ U60 (Algebra.Monoid U60)

Além disso, essas definições relativas são relativas ao path que vc ta executando o compilador isso é bem ruim no sentido que se eu quiser executar um o arquivo checker.kind2 dentro da pasta Wikind/Kind/Checker com o meu path atual sendo Wikind/Checker, isso vai dar erro devido a ele não poder acessar coisas do Wikind como List. A gente poderia consertar isso usando busca na direção inversa por um Wikind.toml que definiria o projeto e o root de procura.

Um exemplo

use Algebra.Laws as Laws
use Algebra.Monoid as Monoid

/identity <t> (monoid: Monoid/ t): Laws/Identity t (/concat monoid) (/empty monoid)
/identity t (/new t_ sg empty id) = id

Adição automática ao contexto.

A coisa que eu PESSOALMENTE mais odeio (e que curiosamente o Taelin tem uma opinião diametralmente oposta a minha) é a adição de nomes ao contexto sem eu citar os nomes, por exemplo, caso eu tente fazer match ou open em algo, como, por exemplo, uma lista,

match List lista {
  cons => // Nesse lugar lista.head e lista.tail estão no contexto
  nil => ..
}

// Podendo ser usada da forma extendida como

match List lista = OUTRACOISA {
  cons => // Nesse lugar lista.head e lista.tail estão no contexto
  nil => ..
} : MOTIVO

AVISO Ignore o MOTIVO no match acima que é opcional e util para algumas situações bem especificas.

nesse lugar os nomes lista.head e lista.tail estão disponíveis no contexto, apesar de eu nunca ter definido eles. O nome vem automaticamente da junção entre lista descrito no escrutinador do match com o nome definido no tipo que seria head e tail. A crítica do Taelin sobre um prmieiro design que eu fiz do match é a de que o match em um construtor enorme daria bem errado. Por exemplo:

/// Imagina que eu tenho um tipo chamado CentopeiaEnormeAssasina que tem 100 campos (pq eu tenho que
/// manter o tracking de cada uma das 100 pernas de forma eficiente). Então eu teria algo assim:
match CentopeiaEnormeAssasina centopeia {
  create _ segunda_perna _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => ..
} : MOTIVO

Para evitar que essas coisas sejam adicionadas automaticamente no contexto, e tbm não ter que colocar um nome para cada perna da incrível centopéia, proponho a mudança da sintaxe para:

// Nesse exemplo, CentopeiaEnormeAssasina tem um construtor chamado `create` que tem argumentos `perna1: U60` e `perna2: U60` em
// sua definição. 

match CentopeiaEnormeAssasina centopeia {
  create perna1 (perna2: perna_bugada) .. => ..
} : MOTIVO

// Talvez com {primeiro, segundo: outro_nome} ao invés disso?

Além disso, gostaria de trocar o open por um let com destructuring similar ao match como:

// Talvez sem {} ao redor? tem que ser o mesmo nome do field ai eu nao tenho certeza se devemos tirar ou não.
let User { name } = user
name

Paths e definições.

Uma coisa que eu considero meio complicada de lidar hoje em dia é a questão dos derives gerarem bastante boilerplate e os .type serem externos a linguagem. Para resolver esse problema eu gostaria de propor que os .types fossem construções de top level da linguagem como qualquer entry, mas, para isso ser possível, vamos ter que mudar como que os construtores são encontrados dentro da linguagem. Ao invés de List.cons só procurar no arquivo exato List/cons.kind2, precisariamos procurar de forma sequencial:

Procura no List/cons.kind2 e caso não ache, ele segue pro List.kind2 e caso seja uma pasta ele desiste. Uma terceira etapa seria procurar no List/_.kind2 mas não acho que seja muito necessário esse tipo de arquivo, podemos definir List em List.kind2 e as funçoes que utilizam ele em List/bla.kind2.

Um exemplo de como ficaria sendo top level dentro de um arquivo chamado Wikind/Vector.kind2.

// Esse é um exemplo mais complexo com indices e que deriva Show
// que seria um "stringifier" para o seu tipo :)

#derive = [Show]
type Vector <ty> ~ (n: Nat) {
  cons <size: Nat> (head: ty) (tail: Vec ty size) ~ Vec ty (Nat.succ size)
  nil ~ Vec ty Nat.zero
}

record User <n: Seila> {
  name: String
  age: U60
  data: n
}

Melhorias de uso de Holes

Tem problemas bem tristes ao usar holes como:

Testing (a: Type) : Type
Testing.new (a: Type) (val: a) : (Testing a)

Testing.pure <a> (x: a) : Testing _ { Testing.new a x }
Testing.example : Testing U60 { Testing.pure Unit Unit.new }

Que vão ser melhorados quando eu entender sobre higher order unification e pattern unification :)

Checagem de coverage

É algo que eu sofro pra tentar implementar. Estou estudando o paper "Elaborating dependent (co)pattern matching" e tentando achar uma implementação eficiente, até eu achar, eu vou demorar bastante tempo por isso sorry D:

Geração de documentação

Espero que talvez o Rodrigo consiga depois fazer com que a pagina de documentação de funções aceite um formato que vai ser gerado a partir de códigos em kind que contém comentários com 3 barras por exemplo

Record fields sem getters e setters, remoção do nome dos tipos do Do, Match e Open.

Pra isso precisamos de elaboration no type checker e isso tornaria ele 100% mais lento :\ Precisamos de soluções que sejam rapidas de fazer e... atualmente não temos. Isso é um problema em aberto que vamos ter que INOVAR DEMAIS pra conseguir resolver então ta ai um problema pra vc que ta lendo me ajudar a resolver kskdskdsk

/// Isso apareceria no site! Como docmentação do "Seila". Seria legal aceitar markdown tbm :)
Seila : U60
Seila = 2

Attributes

Attributes são formas de dar pro compiler algumas tarefas a mais, por exemplo, aliases para compilação a kdl podem ser attributes assim como o estado inicial e etc.

#kdl_name = "PUDIM"
MegaBlasterPudim : U60
MegaBlasterPUDIM = U60

Outras ideias

• LSP (Eu amo LSP e acho que seria bem útil pra todo mundo)
• REPL