mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
Merge pull request #329 from miguel-nascimento/markdown-highlight
syntax highlight in blog posts
This commit is contained in:
commit
c71daa1809
@ -61,7 +61,7 @@ your Haskell programs. For example, the
|
||||
[`Example.fm`](https://github.com/moonad/Formality/blob/master/src/Example.fm)
|
||||
file has the following definition:
|
||||
|
||||
```c
|
||||
```javascript
|
||||
Example.sum(n: Nat): Nat
|
||||
case n {
|
||||
zero: 0
|
||||
@ -146,7 +146,7 @@ Formality | Haskell
|
||||
|
||||
By tagged accessors, I mean that, for example, a program like:
|
||||
|
||||
```c
|
||||
```javascript
|
||||
type FooBar {
|
||||
foo(a: String, b: String)
|
||||
bar(n: Nat, m: Nat)
|
||||
|
@ -5,7 +5,7 @@ Sometimes, heterogeneous data types are desirable, even in a strongly typed
|
||||
language. For example, first-class modules could be represented as maps from
|
||||
strings to functions. The problem is, the type of these functions may vary:
|
||||
|
||||
```
|
||||
```javascript
|
||||
IntLib.add(a: Int, b: Int): Int
|
||||
a + b
|
||||
|
||||
@ -33,24 +33,24 @@ values, even though we're in a statically typed language.
|
||||
In a dependently typed language, one way to have this is to implement a
|
||||
`Dynamic` type, which is a pair of `type, value`:
|
||||
|
||||
```
|
||||
```agda
|
||||
data Dynamic : Set where
|
||||
new : (T : Set) -> (value : T) -> Dynamic
|
||||
```
|
||||
|
||||
This datatype is like a box that "hides" a value and its type internally, but is
|
||||
itself viewed as a single type, called `Dynamic`. This, in turn, allows us to
|
||||
itself viewed as a single type, called `Dynamic`. This, in turn, allows us to
|
||||
create collections of types that vary. For example, we may store ints and
|
||||
strings in the same `List Dynamic`:
|
||||
|
||||
```
|
||||
```agda
|
||||
elems : List Dynamic
|
||||
elems = [new Int 3, new String "foo"]
|
||||
```
|
||||
|
||||
We can also make functions to extract the type and the value of a `Dynamic`:
|
||||
|
||||
```
|
||||
```agda
|
||||
typeOf : Dynamic -> Set
|
||||
typeOf (new T value) = T
|
||||
|
||||
@ -60,7 +60,7 @@ valueOf (new T value) = value
|
||||
|
||||
And we can use `valueOf` to recover a typed value from a "static dynamic":
|
||||
|
||||
```
|
||||
```agda
|
||||
dyn : Dynamic
|
||||
dyn = new Int 7
|
||||
|
||||
@ -78,7 +78,7 @@ since we're always able to cast module functions to their actual types.
|
||||
|
||||
If we blindly translate the program above to Kind, this is what we get:
|
||||
|
||||
```
|
||||
```javascript
|
||||
type Dynamic {
|
||||
new<T: Type>(value: T)
|
||||
}
|
||||
@ -120,7 +120,7 @@ $ kind Dynamic.new --show
|
||||
|
||||
Then, we replace the `type Dynamic { ... }` syntax sugar by the terms above:
|
||||
|
||||
```
|
||||
```javascript
|
||||
Dynamic: Type
|
||||
self<P: Dynamic -> Type>
|
||||
(new: <T: Type> (value: T) P(Dynamic.new(T, value)))
|
||||
@ -136,7 +136,7 @@ syntax desugar to it. Now, we hack it by making one small change: we replace
|
||||
`value : T` in the `new` constructor by `value : type_of(self)`. That's because
|
||||
`T` is the first field of `self`, so both are equivalent:
|
||||
|
||||
```
|
||||
```javascript
|
||||
Dynamic: Type
|
||||
self<P: Dynamic -> Type>
|
||||
(new: <T: Type> (value: Dynamic.type_of(self)) P(Dynamic.new(Dynamic.type_of(self), value)))
|
||||
@ -149,7 +149,7 @@ Dynamic.new<T: Type>(value: T): Dynamic
|
||||
This should work in any language with self types. Since not every reader is
|
||||
familiar with Kind's syntax, here is the same code in an Agda-like syntax:
|
||||
|
||||
```
|
||||
```javascript
|
||||
Dynamic : Set
|
||||
Dynamic =
|
||||
∀ self (P : Dynamic -> Set) ->
|
||||
@ -163,7 +163,7 @@ new T value = \ P new -> new T value
|
||||
With this small change, we're now able to extract values of static dynamics just
|
||||
like in Agda. In other words, the following program type-checks just fine:
|
||||
|
||||
```
|
||||
```javascript
|
||||
dyn: Dynamic
|
||||
Dynamic.new<Nat>(7)
|
||||
|
||||
@ -177,6 +177,6 @@ With this, we're able to represent first-class modules in Kind. The `Dynamic`
|
||||
and `Module` modules are already on base. Kind users can already use first-class
|
||||
modules in their codes, and the first snippet in this post works as is!
|
||||
|
||||
As a last thought, I wonder if, in a future, we should desugar the `type`
|
||||
As a last thought, I wonder if, in a future, we should desugar the `type`
|
||||
syntax in a way that does this automatically. I see no reason not to, but
|
||||
it would increase the complexity of the desugarer considerably.
|
||||
|
@ -3,7 +3,7 @@ Funcional Alquimista
|
||||
|
||||
O Haskell e outras linguagens funcionais usam tipos algébricos, declarados com a sintaxe "data":
|
||||
|
||||
```
|
||||
```haskell
|
||||
data Bool = True | False
|
||||
data Jokenpo = Rock | Paper | Scissor
|
||||
data Pair x = MakePair x x
|
||||
@ -17,25 +17,25 @@ Se você não entende o que está acontecendo acima, o resto não vai fazer sent
|
||||
|
||||
Era uma linda tarde de sol, quando um alquimista funcional, como outro qualquer, se perguntou a pergunta que todos fazemos um dia: "se tipos funcionais são chamados algébricos... por que não escrevemos eles como equações algébricas?" Sem saber que essa pergunta lhe levaria a um caminho sem volta que tangeria a porta da verdade, o pobre alquimista pegou um giz e, em seu já desgastado quadro negro, escreveu a seguinte equação:
|
||||
|
||||
```
|
||||
```haskell
|
||||
Bool = 1 + 1
|
||||
```
|
||||
|
||||
Em sua cabeça, isso fez sentido, porque Bool é um tipo soma, que pode ter dois valores: True e False. Na linha abaixo, ele escreveu:
|
||||
|
||||
```
|
||||
```haskell
|
||||
Jokenpo = 1 + 1 + 1
|
||||
```
|
||||
|
||||
Isso também fez sentido, porque existem 3 movimentos no Jokenpo: Rock, Paper, Scissor. Até aí, tudo parecia uma brincadeira inocente. Mas foi na próxima linha que as coisas começaram a ficar... interessantes. Se tipos soma são representados por uma adição, então tipos produto só podem ser representados com...
|
||||
|
||||
```
|
||||
```haskell
|
||||
Pair x = x * x
|
||||
```
|
||||
|
||||
Uma multiplicação! Mas isso realmente funciona? Vamos verificar: de acordo com essa equação, o tipo `Pair Jokenpo Jokenpo` deveria ter um total de `(1 + 1 + 1) * (1 + 1 + 1) = 3 * 3 = 9`, elementos. Vamos contar:
|
||||
|
||||
```
|
||||
```haskell
|
||||
(Rock, Rock)
|
||||
(Rock, Paper)
|
||||
(Rock, Scissor)
|
||||
@ -49,13 +49,13 @@ Uma multiplicação! Mas isso realmente funciona? Vamos verificar: de acordo com
|
||||
|
||||
NANI!? Não pode ser. Será? Na linha abaixo, ele escreveu:
|
||||
|
||||
```
|
||||
```haskell
|
||||
Maybe x = 1 + x
|
||||
```
|
||||
|
||||
De acordo com essa equação, o tipo `Maybe Bool` deveria ter `1 + 2 = 3` elementos. Vamos contar:
|
||||
|
||||
```
|
||||
```haskell
|
||||
Nothing
|
||||
Just True
|
||||
Just False
|
||||
@ -63,13 +63,13 @@ Just False
|
||||
|
||||
Caramba. Mas o que acontece com tipos infinitos?
|
||||
|
||||
```
|
||||
```haskell
|
||||
Nat = 1 + Nat
|
||||
```
|
||||
|
||||
Nesse caso, temos um loop:
|
||||
|
||||
```
|
||||
```haskell
|
||||
Nat = 1 + 1 + Nat
|
||||
Nat = 1 + 1 + 1 + Nat
|
||||
Nat = 1 + 1 + 1 + 1 + ... Nat
|
||||
@ -77,7 +77,7 @@ Nat = 1 + 1 + 1 + 1 + ... Nat
|
||||
|
||||
O que reflete o fato que existem infinitos números naturais. Logo mais, ele descobriu que o mesmo vale para listas e árvores:
|
||||
|
||||
```
|
||||
```haskell
|
||||
List x = 1 + x * List x
|
||||
```
|
||||
|
||||
@ -85,20 +85,20 @@ Pra visualizar essa equação, vamos primeiro contar a quantidade de elementos d
|
||||
|
||||
List Bool de tamanho 0 tem 1 elemento:
|
||||
|
||||
```
|
||||
```haskell
|
||||
[]
|
||||
```
|
||||
|
||||
List Bool de tamanho 1 tem 2 elementos:
|
||||
|
||||
```
|
||||
```haskell
|
||||
[True]
|
||||
[False]
|
||||
```
|
||||
|
||||
List Bool de tamanho 2 tem 4 elementos:
|
||||
|
||||
```
|
||||
```haskell
|
||||
[True,True]
|
||||
[True,False]
|
||||
[False,True]
|
||||
@ -107,7 +107,7 @@ List Bool de tamanho 2 tem 4 elementos:
|
||||
|
||||
List Bool de tamanho 3 tem 8 elementos:
|
||||
|
||||
```
|
||||
```haskell
|
||||
[True,True,True]
|
||||
[True,True,False]
|
||||
[True,False,True]
|
||||
@ -120,13 +120,13 @@ List Bool de tamanho 3 tem 8 elementos:
|
||||
|
||||
Ou seja, ao todo, List Bool tem um total de:
|
||||
|
||||
```
|
||||
```haskell
|
||||
1 + 2 + 4 + 8 + 16 + ...
|
||||
```
|
||||
|
||||
Elementos. Será que isso condiz com a equação acima? Vamos tentar aplicá-la:
|
||||
|
||||
```
|
||||
```haskell
|
||||
List Bool = 1 + 2 * List Bool
|
||||
List Bool = 1 + 2 * (1 + 2 * List Bool)
|
||||
List Bool = 1 + 2 + 4 * List Bool
|
||||
@ -139,13 +139,13 @@ List Bool = ...
|
||||
|
||||
Uau! Nesse momento, o alquimista estava ciente de que havia encontrado algo realmente interessante. Ele estava à beira da porta da verdade, mas ainda havia tempo para voltar: virar de costas, fingir que aquela brincadeira nunca havia acontecido e levar uma vida normal e pacata. Mas o alquimia tinha sede por verdade, e não temia a inquisição. Então, com sangue nos olhos e as mãos tremendo, ele escreveu mais uma linha. Esta linha, eu lhes transcrevo na forma original:
|
||||
|
||||
```
|
||||
```haskell
|
||||
d/dx Pair x = ?
|
||||
```
|
||||
|
||||
Nesse momento, a porta da verdade se abriu.
|
||||
|
||||
```
|
||||
```haskell
|
||||
d/dx Pair x =
|
||||
d/dx (x * x) =
|
||||
d/dx (x²) =
|
||||
@ -154,13 +154,13 @@ d/dx (x²) =
|
||||
|
||||
Essa linha lhe disse que a derivada do tipo par, representado por "x * x", é o tipo representado por "x + x", ou seja:
|
||||
|
||||
```
|
||||
```haskell
|
||||
data DeltaPair x = Fst x | Snd x
|
||||
```
|
||||
|
||||
Mas qual seria a relação desse tipo, com o tipo par? O alquimista, perplexo, pensou por muito tempo, até formular a seguinte teoria: se a derivada de uma função algébrica é uma função capaz de focar em um ponto infinitesimal da função original, então, a derivada de um tipo algébrico deveria ser um tipo capaz de focar em um ponto do tipo original. Isso fez sentido. Afinal, se temos o par `(5, 7)`, então, podemos focar em dois elementos: o da esquerda, `(*, 7)`, ou o da direita, `(5, *)`. Esses dois pontos de foco podem ser representados pelo tipo DeltaPair, como `Fst 7` ou `Snd 5`, respectivamente. Para confirmar essa teoria, o alquimista tentou aplicar o mesmo ao tipo das listas, o que lhe demandou certa ingenuidade algébrica:
|
||||
|
||||
```
|
||||
```haskell
|
||||
List x = 1 + x * List x
|
||||
List x - x * List x = 1
|
||||
List x * (1 - x) = 1
|
||||
|
Loading…
Reference in New Issue
Block a user