teika_help.md

Teika

Uma linguagem funcional, pura, com tipos dependentes e um descendente de ML.

Convenção

Geralmente tipos e coisas que contem tipos começam com letra maiuscula. snake_case para tudo.

Features

Literais

String

Integers

Booleans

Funções

Um tipo unico de funções. Normalmente linguagens tem 2 ou 3 tipos de funções, funções de valores para valores aka funções normais, funções de tipos para valores aka polimorfismo, funções de tipos para tipos.

Teika tem um tipo unico, que permite tanto valor para valor, tipo para valor, tipo para tipo e valor para tipo.

O tipo de funções tem o formato de (x : A) -> B. E funções tem o formato de (x : A) => e. Chamada de função tem o formato de lambda argument.

Funções dependentes, são funções que o tipo do retorno depende no parametro. Funções polimórficas são funções dependentes.

Funções descrevem quantificação universal, aka forall.

// valor para valor, aceita inteiro e retorna inteiro
incr : (x : Int) -> Int = (x : Int) => x + 1;
two = incr 1;
// tipo para valor, aceita um tipo e retorna uma função
id : (A : Type) -> (x : A) -> A = (A : Type) => (x : A) => x;
id_int : (x : Int) -> Int = id Int;
one = id_int 1;
// tipo para tipo, aceita um tipo e retorna ele mesmo
Id = (A : Type) => A;
// o mesmo que Int
Id_int = Id Int;
// valor para tipo, aceita um boolean e o retorno depende no boolean
id_int_or_string :
  (pred : Bool) ->
  (x : pred | true => Int | false => String) ->
  pred | true => Int | false => String =
    (pred : Bool) =>
    (x : pred | true => Int | false => String) => x;
id_int : (x : Int) -> Int = id_int_or_string true;
id_string : (x : String) -> String = id_int_or_string false;

Tuplas nomeadas

São tipos, pares, mas podem ter mais elementos. Diferente da maior parte das linguagens, o valor da direita pode depender no valor da esquerda.

Quando não dependentes, elas funcionam como tuplas normais. E quando for dependente se comportam parecido com modulos ou first class modules em OCaml.

Da mesma forma que funções, tuplas podem ser de valor e valor, tipo e valor, tipo e tipo e valor e tipo.

São sempre nomeadas em Teika.

O tipo de tuplas tem a seguinte forma (x : A, y : B, z : C) Tuplas tem a forma de (x = 1, y = 2). Destructuring de tuplas (x, y, z) = tuple; e;

Descrevem quantificação existencial aka exists.

// valor para valor
center : (x : Int, y : Int) = (x = 0, y = 0);
(x, y) = center;
// tipo para valor
Show = (A : Type, value : A, show : (x : A) -> String);
show : (x : Show) -> String = (x : Show) => (
  (A, value, show) = x;
  show value;
);
show_one : Show = (A = Int, value = 1, show = (x : Int) => Int.to_string x);
one_string = show show_one;
// tipo para tipo
X : (A : Type, B : Type) = (A = Int, B = String);
// valor para tipo
Either = (A : Type) => (B : Type) =>
  (tag : Bool, x : left | true => A | false => B);
to_string = (pair : Either Int String) =>
  pair
  | (tag : true, x) => Int.to_string x
  | (tag : false, x) => x;

Let

Let tem o formato de x = e1; e2. Apenas conveniencia, é equivalente a ((x : A) => e2) e1.

Porém lets são expressão que demandam parenteses.

Se comportam de forma identica a let em OCaml, incluindo shadowing.

f = (x : Int) => (
  y = x;
  y
);

f = (x : Int) => (y : Int) (
  z = (
    // shadowing
    y = y * 2;
    x + y
  );
  z + 1
);

Annot

Anotações sempre demandam parenteses. Tem o formato de (e : A).

x = (1 : Int);
y = ("a" : String);