Thread

Bend – a language that blocks AI mistakes via proof and runs on GPUs

616 points · 327 comments · nicolas-siplis

amluto · 1789680434 · focus · HN ↗
Maybe in our brave new world only the "laws" will matter and the implementation language is irrelevant to humans. In the mean time I have some questions about the "guide", which claims to define the entire language:
<a href="https://github.com/bendlang/bend/blob/main/guide/GUIDE.md" rel="nofollow">https://github.com/bendlang/bend/blob/main/guide/GUIDE.md
Let's see:
- There are no infinite loops, and recursion is kind of softly bounded to 2^48-1. This sounds grrrreat for games. I guess they have to stop working after a while? (What would be wrong with addressing this conceptually like Lean does? Have a way to annotate a term as possibly non-terminating?)
- We seem to have Data and Type and Kind, and they don't mean what they conventionally do. '-' means "used 0 types". And the example is:
```
    def length(a, -A: Kind(a), xs: List&lt;a, A&gt;) -&gt; Nat:
      match xs:
        case Nil{}:
          0n
        case Con{h, t}:
          1n+length(a, A, t)
```
But wait! A is used albeit not at runtime. Is it possible that this actually intends "A may be used any number of times and is itself the name of a - type"? Shouldn't that be spelled "A: Kind(a) & -" or similar? Why does the kind even matter for this example?
- I don't understand the Array example:
```
    import Base
    
    def main() -&gt; Array&lt;U32&gt; &amp; U32:
      a = [0 : U32*8n] # new array with 8 copies of 0
      a[5] &lt;- 42       # performs an in-place rewrite
      a[5]             # reads index 5
```
What is the return type of this function? It looks like it returns U32. So what's "Array<U32> & U32"?
- I don't even understand the Array explanation:
> The slot count after * is a power of two; [0 : U32^3n] names the depth instead.
Okay, the 8 in *8n above is indeed a power of two. Does the language require it? Does it actually mean 2^8? What is the "depth" of an array? Does this language not have non-power-of-two-sized arrays?
At this point I stopped reading.
1. LightMachine · 1789681251 · focus · HN ↗
  Nothing wrong with addressing it conceptually! We will, in the upcoming versions, probably via codata / coroutines. For V1, I'm keeping the language set smell. When it is stable, we'll add more features. Lean had 10+ years to mature; Bend is on day 1.
  `-` means "erased argument". You can use an erased argument as many times as you want, in erased positions. That's also how QTT works (Idris2 is based on it). This example is there precisely to introduce Kinds, which are universes indexed on quantities.
  - Kind(&2) is inhabited by clonable values. - Kind(&1) is inhabited by linear values. - Kind(&0) is like Rocq's Prop.
  `A & B` is just sugar for the pair type former (which is sugar for a sigma).
  Thanks for your questions and patience!
  1. amluto · 1789681703 · focus · HN ↗
    So why does the length function take the ‘a’ parameter (the type of the elements?) and its Kind? Wouldn’t the type imply the kind? Why does the kind matter? Is the - a constraint on the kind? How would the program be different without the -?
    When you say “pair type former” do you mean that Array<U32> & U32 is what Rust would call (Array<U32>, U32)? If so, why does that example function actually return a value of this type? It sure looks like it returns plain U32.
    > You can use an erased argument as many times as you want, in erased positions.
    What’s the rationale for this? Why is an “erased” position special? What is an erased position, anyway?
    ISTM if I want to use an affine term that has zero size at runtime as a token that may be used at most once, I think I wouldn’t want an exception for using it in an “erased” position. Can I have a function like a -> a & a where the input is “erased”?
    [deleted] · 1789686190 · focus · HN ↗
    [deleted]

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.