just did a map using two lists as input! logic programming is cooool
having fun playing with makam:
Conversation
Replying to
Now playing with some declarative typing rules for Martin-Löf type theory in Makam! Finally starting to get my head around why they are defined the way they are, I think? Not sure if I want to use explicit substitutions yet, hence the commented out declarations… 🤔
1
1
I'm _thinking_ that these general rules mean that you don't have to write as many duplicated rules for things like booleans. For example if we write an elimination rule with the eliminator on the left, we get the one on the right for free, thanks to the symmetry rules:
1
As somebody who often reads type theory papers and books by trying to get as quickly to "how do I implement this?" as possible, this is a rather cool way to think about stuff, even if it's a bit weird and different!
2
Oh not before! I think it introduces data types in a similar way to Makam and λProlog right? What made you bring it up?
1
Show replies
Replying to
It's interesting that check and synth end up having the same signature here...
1
1
yeah, they have different modes though - like:
check : in -> in -> in -> mode.
synth : in -> in -> out -> mode.
(if Makam had support for this, like in Mercury)
2
Show replies