One high-level connection I’ve been investigating ...
# of-logic-programmingw
Will
09/17/2020, 4:11 PMOne high-level connection I’ve been investigating is functional programming <-> logic programming. Languages like Rust and Haskell have a Prolog-esque logic programming language in their type system via traits/typeclasses. This allows you to do some cool type-level programming (distinct from compile-time metaprogramming and partial evaluation!!), but writing raw traits is super gnarly. So I’ve been working on a language to bridge the gap: https://github.com/willcrichton/tyrade
👍 4
Will
09/17/2020, 4:13 PMSee the Rust book if you’re interested for more details on the logic programming language in Rust: http://rust-lang.github.io/chalk/book/clauses.html
w
wtaysom
09/18/2020, 2:57 AMWow! Sometimes, I feel we would be well served by starting with a logic language then using it for types. What are types anyway? (The digression I'm about to start into does not belong in a thread.)
n
Nick Smith
09/18/2020, 9:18 AMType systems are a form of static analysis, and some would argue static analysis is best performed in a logic language (see Soufflé). That's what I understand Rust is doing with Chalk, but only after the type system was already designed!
Nick Smith
09/18/2020, 9:22 AMWhat if type-level programs and ordinary programs were all written in the same language? Seems do-able if the programming language is a logic language.
Nick Smith
09/18/2020, 9:25 AMTyrade is essentially that? Using macros to make type signatures look like ordinary Rust functions?
j
James Sully
09/20/2020, 5:04 PMIdris is another language trying to bridge that gap!
2 Views