6 ms·

Kei – A small and expressive dependent language

67 points by caotic 7y ago

GreeniFi 7y ago
An unusual name. Is it a reference to the Kei River in South Africa’s Eastern Cape? Sorry - bit of a random question.
- jogu 7y ago
  It's one of the readings of the Japanese character 軽, which means light (as in not heavy). That would be my guess, but I can't say for certain.
- benj111 7y ago
  "The core of Key is based on a ....." So either it was called key, and Kei is a homophone, or visa versa, thus the mispelling or 2 translations from a different language, or they really like Kei cars ?
  - protomyth 7y ago
    Or autocorrect interfered
- enz 7y ago
  The same kei (軽, lightweight) as kei-car, maybe: https://en.m.wikipedia.org/wiki/Kei_car https://en.m.wikipedia.org/wiki/Kei_car
- Gys 7y ago
  Its Dutch it means 'stone' or 'rock'. Its often used as 'kei-goed' meaning very, very good. So in Dutch its actually great language name!
- caotic 7y ago
  It's Kei (romaji) meaning light. I don't remember where I get that name, but I think I was listening to some random music.
mkorfmann 7y ago
> One of the most interesting properties of Kei is you can combine statics symbols with rewriting rules to create another logic system, like COC. In λΠ-calculus modulo the conversion of terms is available between β-reduction and Γ-Reduction, this means that a type can be changed through a type relation of a rewriting rule. Of course, if there is a well-typed substitution rule σ(x). Where is the <1% of the world population who can translate this to human-speak, when you need them?
- Etheryte 7y ago
  I tried looking into this, but this publication's abstract [1] is just as (un)helpful: > The lambda-Pi-calculus Modulo is a variant of the lambda-calculus with dependent types where beta-conversion is extended with user-defined rewrite rules. It is an expressive logical framework and has been used to encode logics and type systems in a shallow way. Basic properties such as subject reduction or uniqueness of types do not hold in general in the lambda-Pi-calculus Modulo. However, they hold if the rewrite system generated by the rewrite rules together with beta-reduction is confluent. [...] [1] https://arxiv.org/abs/1507.08055 https://arxiv.org/abs/1507.08055
  - aisofteng 7y ago
    This is standard language that is perfectly readable if you’re familiar with the involved concepts.
    - mkorfmann 7y ago
      Since you are a member of the 1% who understands this, please help us mumbo dumbos.
      - xelxebar 7y ago
        tl;dr: Looks like they are trying to formally encode the notion of "rewrite rule" within type theory itself. Also a mumbo dumbo here, but I might be able to say something helpful. This is a bit of long post as I am trying to provide some context. A useful way to think of logic and type systems is simply as rewrite rules on arbitrary strings. In logic we call these strings "theorems" and in type theory we call them "types". In particular, say we have the logical theorem "a /\ (a -> b)". In classical (propositional) logic this corresponds to "a implies b, and a is true", so we make the (obvious) deduction that "b" is true. In other words, we rewrite "a /\ (a -> b)" with the string "b". Intuitively, we want to say the above rewrite means the same thing as "(a /\ (a -> b)) -> b". However, the former is a rewrite while the later is just a static string. Thus we are forced to distinguish between the formal "->" character and the rewrite process, despite these naively/intuitively both meaning inference. A bit of terminology. Classically, we call strings "theorems" and when we rewrite one string for another, we call that a "deduction". So say we have a string "S" and rewrite it as "T", a common way of notating such a deduction is "S => T". Furthermore, the whole system of deductions is what we call our "metalogic" while the collection of theorems produced is our "formal logic". Anyway, so we have to distinguish between "->" and "=>", which seems a bit unfortunate. There is this standard tool in classical logic called the Deduction Theorem which adds a rule that given "S => T" we can deduce "S -> T". However, the justification for this uses somewhat sophisticated math and, by necessity, it's an argument in some (meta)metalogic. There are other ways of handling this and metalogics that don't have the Deduction Theorem at all. I have even read that Quantum Logic doesn't have such a rule and that adding it in turns the whole system into classical logic! Now, to finally get to the point, Kei looks like it uses a metalogic it's calling "λ-Calculus Modulo Theory" which ports the Deduction Theorem to type theory, or in particular, the dependently typed λ-calculus. They seem to be calling these new rules Γ-reduction. In other words, it attempts to make general rewrite rules, like β-reduction, first-class citizens by adding types that correspond to said rules. If I'm understanding correctly, one attractive feature of this is that it "closes the loop," per se, allowing one to encode their λ-Calculus Modulo Theory within itself, which by extension, let's us encode any other λ-calculus as well. Ostensibly, this should allow for maximally compact and expressive types, since you don't have to hack simple metalogical concepts into a less powerful type system. I only skimmed their paper, but in general one could use their system to model some badly-behaved (i.e. non-confluent) type theories; however, they seem to have a (meta)theorems showing that certain uses of the Γ-reduction give you well-behaved ones.
jsjolen 7y ago
Can someone read out to me how the Abstraction rule works?

67 points by caotic 7y ago

GreeniFi 7y ago

An unusual name. Is it a reference to the Kei River in South Africa’s Eastern Cape? Sorry - bit of a random question.

jogu 7y ago
It's one of the readings of the Japanese character 軽, which means light (as in not heavy). That would be my guess, but I can't say for certain.
benj111 7y ago
"The core of Key is based on a ....." So either it was called key, and Kei is a homophone, or visa versa, thus the mispelling or 2 translations from a different language, or they really like Kei cars ?
- protomyth 7y ago
  Or autocorrect interfered
enz 7y ago
The same kei (軽, lightweight) as kei-car, maybe: https://en.m.wikipedia.org/wiki/Kei_car https://en.m.wikipedia.org/wiki/Kei_car
Gys 7y ago
Its Dutch it means 'stone' or 'rock'. Its often used as 'kei-goed' meaning very, very good. So in Dutch its actually great language name!
caotic 7y ago
It's Kei (romaji) meaning light. I don't remember where I get that name, but I think I was listening to some random music.

mkorfmann 7y ago

> One of the most interesting properties of Kei is you can combine statics symbols with rewriting rules to create another logic system, like COC. In λΠ-calculus modulo the conversion of terms is available between β-reduction and Γ-Reduction, this means that a type can be changed through a type relation of a rewriting rule. Of course, if there is a well-typed substitution rule σ(x). Where is the <1% of the world population who can translate this to human-speak, when you need them?

Etheryte 7y ago
I tried looking into this, but this publication's abstract [1] is just as (un)helpful: > The lambda-Pi-calculus Modulo is a variant of the lambda-calculus with dependent types where beta-conversion is extended with user-defined rewrite rules. It is an expressive logical framework and has been used to encode logics and type systems in a shallow way. Basic properties such as subject reduction or uniqueness of types do not hold in general in the lambda-Pi-calculus Modulo. However, they hold if the rewrite system generated by the rewrite rules together with beta-reduction is confluent. [...] [1] https://arxiv.org/abs/1507.08055 https://arxiv.org/abs/1507.08055
- aisofteng 7y ago
  This is standard language that is perfectly readable if you’re familiar with the involved concepts.
  - mkorfmann 7y ago
    Since you are a member of the 1% who understands this, please help us mumbo dumbos.
    - xelxebar 7y ago
      tl;dr: Looks like they are trying to formally encode the notion of "rewrite rule" within type theory itself. Also a mumbo dumbo here, but I might be able to say something helpful. This is a bit of long post as I am trying to provide some context. A useful way to think of logic and type systems is simply as rewrite rules on arbitrary strings. In logic we call these strings "theorems" and in type theory we call them "types". In particular, say we have the logical theorem "a /\ (a -> b)". In classical (propositional) logic this corresponds to "a implies b, and a is true", so we make the (obvious) deduction that "b" is true. In other words, we rewrite "a /\ (a -> b)" with the string "b". Intuitively, we want to say the above rewrite means the same thing as "(a /\ (a -> b)) -> b". However, the former is a rewrite while the later is just a static string. Thus we are forced to distinguish between the formal "->" character and the rewrite process, despite these naively/intuitively both meaning inference. A bit of terminology. Classically, we call strings "theorems" and when we rewrite one string for another, we call that a "deduction". So say we have a string "S" and rewrite it as "T", a common way of notating such a deduction is "S => T". Furthermore, the whole system of deductions is what we call our "metalogic" while the collection of theorems produced is our "formal logic". Anyway, so we have to distinguish between "->" and "=>", which seems a bit unfortunate. There is this standard tool in classical logic called the Deduction Theorem which adds a rule that given "S => T" we can deduce "S -> T". However, the justification for this uses somewhat sophisticated math and, by necessity, it's an argument in some (meta)metalogic. There are other ways of handling this and metalogics that don't have the Deduction Theorem at all. I have even read that Quantum Logic doesn't have such a rule and that adding it in turns the whole system into classical logic! Now, to finally get to the point, Kei looks like it uses a metalogic it's calling "λ-Calculus Modulo Theory" which ports the Deduction Theorem to type theory, or in particular, the dependently typed λ-calculus. They seem to be calling these new rules Γ-reduction. In other words, it attempts to make general rewrite rules, like β-reduction, first-class citizens by adding types that correspond to said rules. If I'm understanding correctly, one attractive feature of this is that it "closes the loop," per se, allowing one to encode their λ-Calculus Modulo Theory within itself, which by extension, let's us encode any other λ-calculus as well. Ostensibly, this should allow for maximally compact and expressive types, since you don't have to hack simple metalogical concepts into a less powerful type system. I only skimmed their paper, but in general one could use their system to model some badly-behaved (i.e. non-confluent) type theories; however, they seem to have a (meta)theorems showing that certain uses of the Γ-reduction give you well-behaved ones.

jsjolen 7y ago

Can someone read out to me how the Abstraction rule works?