7 ms·

> So, a good place to try and understand underlying linguistic structure is informal mathematics, something he studied in his 1993 paper Type theory and the inf

> So, a good place to try and understand underlying linguistic structure is informal mathematics, something he studied in his 1993 paper Type theory and the informal language of mathematics. This investigates both directions of the passage between formal and informal mathematics: sugaring and formalization. Okay... > x:A ⊢ B(x): Type I'm lost.

icen 6y ago
This is standard notation. The `x : A` supposes a value, `x`, inhabiting a type `A` (like in Rust, or ML, or maybe `A x` in C). On the right hand side of the turnstile, we have `B(x) : Type`, which is roughly what it looks like: `B` is a type parameterised by `x` (note - it is not parameterised by `A`, but by `x`! It is allowed to know about the value `x`). The central turnstile is a contextual relation. The left hand side is an ambient known value, and the right hand side is something that be defined in that context. You can read it informally as "given", so this phrase is "given x: A, we can construct a type B(x)".
deleted 6y ago
[deleted]
curryhoward 6y ago
Unfortunately you need to know type theory/logic notation in order to read this. Here's the English translation: - There is a variable called `x` in scope. - `x` is known to have type `A`. - `B` is a function that, when given `x` as an argument, returns a type. If this seems weird, it's because you need dependent types to even be able to say this. Honestly, this article is not written for programmers, and I don't know why it's on Hacker News right now. Most HN readers don't have the necessary background to follow it.
- Gravityloss 6y ago
  Thank you, it is easy to understand when explained like that! Maybe there could be a programming language where these concepts were used but slightly more explicitly, verbosely or in general easier to read fashion. A lot of successful languages are big on ergonomics or low barriers for entry.
  - icen 6y ago
    If you're passingly familiar with Haskell or similar languages, you could give Idris a try. https://www.idris-lang.org/ https://www.idris-lang.org/
  - kungato 6y ago
    Unfortunately, it often seems like "low barrier to entry" means "no prior effort invested" even if it means knowing basic logic notation which is taught in gymnasiums
    - Gravityloss 6y ago
      Hmm, is that symbol basic logic notation, and were you taught that symbol in high school? Which one of these? Do you type it often? https://en.wikipedia.org/wiki/Turnstile_(symbol) https://en.wikipedia.org/wiki/Turnstile_(symbol)
    - nyanpasu64 6y ago
      Is a gymnasium a school in Europe? It's an exercise facility in the USA. I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
      - mcaruso 6y ago
        > Is a gymnasium a school in Europe? It's an exercise facility in the USA. https://en.wikipedia.org/wiki/Gymnasium_(school) https://en.wikipedia.org/wiki/Gymnasium_(school) > I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before. Interesting. I was taught ⊢ first semester in CS in Logic class. Along with most other common logic notation.
      - throwawaygh 6y ago
        > Is a gymnasium a school in Europe? It's an exercise facility in the USA. https://en.wikipedia.org/wiki/Gymnasium_(Germany) https://en.wikipedia.org/wiki/Gymnasium_(Germany) And yes, teaching basic notation from mathematical logic is pretty standard in Gymnasium's. I've taught sequent calculi at US high school enrichment programs; honestly, the students get it perfectly fine. The notation is no more difficult to understand than a two column proof. It's always the teachers who struggle. Every attempt at math ed reform in the US meets that crux -- the teachers' and parents' willingness/ability to learn anything new is always massively over-estimated. The only way to teach real mathematics in US high schools is to smuggle it in through "enrichment" programs. > I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before. Discrete math courses are different from university to university; sometimes formal logic is covered, and sometimes it's more of an "introduction to basic proof techniques and combinatorics" course. A university course in logic should certainly have shown you a sequent calculus at some point. I'm actually confused about how you would fill a semester-long course on logic without a turnstile ever showing up. What notation were you using to write down your derivations? They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium.
- rustybolt 6y ago
  Yes, god forbid if anyone tries to post something that needs some kind of knowledge!
- mcphage 6y ago
  So `A` is a type, and `Type` is a type?
  - throwaway17_17 6y ago
    In this context, ‘A’ is an instance of Type, and ‘Type’ is the type of types (usually the term used for type of type is Kind). So while ‘x’ could be the value 7 and ‘A’ could be the type Int, the ‘B(x):Type’ means that the value of B(x) is some Type, could be Int, Char, Bool, etc.
    - mcphage 6y ago
      Thank you!
  - curryhoward 6y ago
    `A` is a type, yes. Whether `Type` is a type depends on what type system you're working in. If `Type` is its own type, then it turns out you can use that to do infinite recursion (this is called Girard's paradox). Dependent types are often used for proving theorems, where infinite recursion corresponds to circular reasoning—a big no-no. So, in many dependently typed languages, `Type` is not its own type (instead, it's common to have an infinite tower of types: `42` has type `Int`, `Int` has type `Type0`, `Type0` has type `Type1`, `Type1` has type `Type2`, and so on). However, if the programming language is just used for programming and not for proving, then it's perfectly fine (and quite convenient) to have `Type` be its own type.
- fastball 6y ago
  I mean, the syntax really isn't that far off from how you might describe this in programming. To describe this with Python's type hints, for example, you would write this: def B(x: A) -> Type:
carapace 6y ago
It's part of an arcane knowledge that is seldom reified. "It's Time for a New Old Language" – Guy Steele [video] (youtube.com) https://www.youtube.com/watch?v=dCuZkaaou0Q https://www.youtube.com/watch?v=dCuZkaaou0Q https://news.ycombinator.com/item?id=15473199 https://news.ycombinator.com/item?id=15473199 He calls it "Computer Science Metanotation".
dwb 6y ago
What is your point exactly? My response, when faced with something like this, is to be excitedly curious, and try to find out what the notation means, maybe by searching "type theory notation" and going a couple of links deep to find at least the start of an explanation – not to publicly throw up my hands on a comment thread. If I was really at a loss I might ask for some pointers to introductions to the topic. The article is clearly written for people at least somewhat familiar with the domain and notation, and a bit of research shows that it's quite standard notation.
vmchale 6y ago
> I'm lost. Okay

icen 6y ago

This is standard notation. The `x : A` supposes a value, `x`, inhabiting a type `A` (like in Rust, or ML, or maybe `A x` in C). On the right hand side of the turnstile, we have `B(x) : Type`, which is roughly what it looks like: `B` is a type parameterised by `x` (note - it is not parameterised by `A`, but by `x`! It is allowed to know about the value `x`). The central turnstile is a contextual relation. The left hand side is an ambient known value, and the right hand side is something that be defined in that context. You can read it informally as "given", so this phrase is "given x: A, we can construct a type B(x)".

deleted 6y ago

[deleted]

curryhoward 6y ago

Unfortunately you need to know type theory/logic notation in order to read this. Here's the English translation: - There is a variable called `x` in scope. - `x` is known to have type `A`. - `B` is a function that, when given `x` as an argument, returns a type. If this seems weird, it's because you need dependent types to even be able to say this. Honestly, this article is not written for programmers, and I don't know why it's on Hacker News right now. Most HN readers don't have the necessary background to follow it.

Gravityloss 6y ago
Thank you, it is easy to understand when explained like that! Maybe there could be a programming language where these concepts were used but slightly more explicitly, verbosely or in general easier to read fashion. A lot of successful languages are big on ergonomics or low barriers for entry.
- icen 6y ago
  If you're passingly familiar with Haskell or similar languages, you could give Idris a try. https://www.idris-lang.org/ https://www.idris-lang.org/
- kungato 6y ago
  Unfortunately, it often seems like "low barrier to entry" means "no prior effort invested" even if it means knowing basic logic notation which is taught in gymnasiums
  - Gravityloss 6y ago
    Hmm, is that symbol basic logic notation, and were you taught that symbol in high school? Which one of these? Do you type it often? https://en.wikipedia.org/wiki/Turnstile_(symbol) https://en.wikipedia.org/wiki/Turnstile_(symbol)
  - nyanpasu64 6y ago
    Is a gymnasium a school in Europe? It's an exercise facility in the USA. I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before.
    - mcaruso 6y ago
      > Is a gymnasium a school in Europe? It's an exercise facility in the USA. https://en.wikipedia.org/wiki/Gymnasium_(school) https://en.wikipedia.org/wiki/Gymnasium_(school) > I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before. Interesting. I was taught ⊢ first semester in CS in Logic class. Along with most other common logic notation.
    - throwawaygh 6y ago
      > Is a gymnasium a school in Europe? It's an exercise facility in the USA. https://en.wikipedia.org/wiki/Gymnasium_(Germany) https://en.wikipedia.org/wiki/Gymnasium_(Germany) And yes, teaching basic notation from mathematical logic is pretty standard in Gymnasium's. I've taught sequent calculi at US high school enrichment programs; honestly, the students get it perfectly fine. The notation is no more difficult to understand than a two column proof. It's always the teachers who struggle. Every attempt at math ed reform in the US meets that crux -- the teachers' and parents' willingness/ability to learn anything new is always massively over-estimated. The only way to teach real mathematics in US high schools is to smuggle it in through "enrichment" programs. > I've gone through high school and taken CS (and a bit of discrete math and logic) in college, and never seen the ⊢ symbol before. Discrete math courses are different from university to university; sometimes formal logic is covered, and sometimes it's more of an "introduction to basic proof techniques and combinatorics" course. A university course in logic should certainly have shown you a sequent calculus at some point. I'm actually confused about how you would fill a semester-long course on logic without a turnstile ever showing up. What notation were you using to write down your derivations? They used to say "the US has the best high schools in the world; unfortunately, they're called universities". But the universities have become so watered down that many Americans get university degrees without ever passing through an institution at the level of a good gymnasium.
rustybolt 6y ago
Yes, god forbid if anyone tries to post something that needs some kind of knowledge!
mcphage 6y ago
So `A` is a type, and `Type` is a type?
- throwaway17_17 6y ago
  In this context, ‘A’ is an instance of Type, and ‘Type’ is the type of types (usually the term used for type of type is Kind). So while ‘x’ could be the value 7 and ‘A’ could be the type Int, the ‘B(x):Type’ means that the value of B(x) is some Type, could be Int, Char, Bool, etc.
  - mcphage 6y ago
    Thank you!
- curryhoward 6y ago
  `A` is a type, yes. Whether `Type` is a type depends on what type system you're working in. If `Type` is its own type, then it turns out you can use that to do infinite recursion (this is called Girard's paradox). Dependent types are often used for proving theorems, where infinite recursion corresponds to circular reasoning—a big no-no. So, in many dependently typed languages, `Type` is not its own type (instead, it's common to have an infinite tower of types: `42` has type `Int`, `Int` has type `Type0`, `Type0` has type `Type1`, `Type1` has type `Type2`, and so on). However, if the programming language is just used for programming and not for proving, then it's perfectly fine (and quite convenient) to have `Type` be its own type.
fastball 6y ago
I mean, the syntax really isn't that far off from how you might describe this in programming. To describe this with Python's type hints, for example, you would write this: def B(x: A) -> Type:

carapace 6y ago

It's part of an arcane knowledge that is seldom reified. "It's Time for a New Old Language" – Guy Steele [video] (youtube.com) https://www.youtube.com/watch?v=dCuZkaaou0Q https://www.youtube.com/watch?v=dCuZkaaou0Q https://news.ycombinator.com/item?id=15473199 https://news.ycombinator.com/item?id=15473199 He calls it "Computer Science Metanotation".

dwb 6y ago

What is your point exactly? My response, when faced with something like this, is to be excitedly curious, and try to find out what the notation means, maybe by searching "type theory notation" and going a couple of links deep to find at least the start of an explanation – not to publicly throw up my hands on a comment thread. If I was really at a loss I might ask for some pointers to introductions to the topic. The article is clearly written for people at least somewhat familiar with the domain and notation, and a bit of research shows that it's quite standard notation.

vmchale 6y ago

> I'm lost. Okay