Channels

administrivia

announcements

bot-dark-forest

devlog-together

in-alberta

in-boston

in-germany

in-israel

in-london

in-nyc

in-ontario

in-seattle

in-sf

in-socal

introduce-yourself

linking-together

of-ai

of-end-user-programming

of-functional-programming

of-graphics

of-logic-programming

of-music

present-company

random-encounters

reading-together

share-your-work

thinking-together

two-minute-week

wormholes

Title

c

Chris G

05/23/2022, 11:20 PM"Yatima is a pure functional programming language implemented in Rust with... content addressing, first-class types, linear, affine and erased types, type-safe dependent metaprogramming"

```
type Vector (A: Type): ∀ (ω k: Natural) -> Type {
Nil: Vector A Natural.Z,
Cons (0 k: Natural) (x: A) (xs: Vector A k): Vector A (Natural.S k),
}
def Vector.head (0 A: Type) (k: Natural) (a : Vector A (Natural.S k)): A
= ((case a) (λ k' self => ∀ (Equal Natural (Natural.S k) k') -> A)
(λ e => Empty.absurd A (Natural.Z_isnt_S k e))
(λ k x xs e => x))
(Equal.Refl Natural (Natural.S k))
```

https://github.com/yatima-inc/yatima-lang-alpha👀 2