Conversation

Hillel
@hillelogram
I hate to ruin a good shitpost but now that I think about it, it *is* kinda weird that ideas from FP are regularly crossbred into "OOP" languages, while ideas from LP are not Suggests LP is much "further" from FP&OOP than they are from each other
21
62
Joe Groff
@jckarter
Logic programming languages get crossbred with other languages all the time. They just get called “type systems”
2
16
david barsky
@endsofthreads
at the risk of over-explaining something you already know, it’s helpful to view swift’s/rust’s/haskell’s protocols/traits/typeclasses as a form of prolog, which has the side effect (for me!) of making debugging compiler errors way easier
1
7
david barsky
@endsofthreads
a bound on a generic type like `where T: Clone + Hash` is effectively a prolog query that requires the programmer and compiler to work together to pass in a type that implements both the Clone and Hash traits (if this doesn’t make sense, sorry. i blame my insobriety)
1
4
Hillel
@hillelogram
But isn't the thing with logic programming that you don't have to do this? It should tell you whether or not such a type exists, not force you to give it an example. (Caveat: Type theory is a HUGE blind spot of mine)
4
david barsky
@endsofthreads
type systems can’t solve arbitrary expressions for you, but they _can_ tell you via an error message what types can fit for given constraint or explain why the type you passed in doesn’t fit the generic constraint as written
2
1
Hillel
@hillelogram
I guess my confusion is that I thought the solving is what makes logic programming a distinct thing, and without that, it's not LP Tagging
@arntzenius
as a person who knows both type systems and logic programming very well
1
1
david barsky
@endsofthreads
i’m obviously not an expert in this space, but my intuition is that type systems care about checking, not solving, logic. (my understanding is that, under the hood, “checking” is a bounded and directed form of “solving” for tractability reasons)
2
2