5 ms·
Simple Type Inference in 21 Lines of Clojure
- fogus 15y agoMacros and logic engine versus type system... to the death.
- davidmathers 15y agoExplain.
- swannodette 15y agoYou can get a typed Lisp with just macros, see Typed Racket. What's interesting is whether macros + logic engine will allow a programmer to devise much more powerful guarantees than is possible in any specific type system.
- evangineer 15y agoHmm, is anybody aware of any relevant literature on this?
- swannodette 15y agoThere's hardly anything out there from what I can tell. I think because few people understand macros and even fewer understand logic programming. When I saw Oleg Kiselyov's miniKanren type-checker/inferencer/reconstructor in ~300 LOC, the possibilities seemed and still seem endless. Prolog as general programming paradigm has problems - Prolog/Datalog as a way for programmers to reason about their own programs is an untapped goldmine.
- chipsy 15y agoSimilar to my thoughts lately. We have a UI problem to solve, not a paradigm problem. We don't want provability or inference as the first approach to problems - slapping something together with a mix of mutable/functional code is Good Enough to start understanding the domain. But once the solution is complex, and it's necessary to improve iteration times and lower error rates, it tends to be too hard to jury-rig deeper logical properties into existing languages; it leads to mucking about with the build system and compilation process at a deep level, which adds a ton of extra complexity. The "now you have two problems" quote comes to mind.
- rikthevik 15y agoI think that with ten pages of documentation, the author might really be on to something here.
- swannodette 15y agoYes, core.logic is definitely in need of more documentation. However it is under heavy development and I'm still unwilling to commit to some design choices just yet. Even with documentation, I'll never be able to do justice to the art of logic programming - if you're willing to pick up The Reasoned Schemer you'll understand exactly how core.logic works and any good Prolog book will take you the rest of the way.
- swannodette 15y agoAuthor there. Let me explain - core.logic is a Prolog-like logic engine written in Clojure. It is in fact so similar to Prolog that it's actually quite trivial to port Prolog code as I've done here. The other nice bit is that core.logic is quite fast - it is not the toy implementation of Prolog that you see so often. UPDATE: edited the examples to show concrete types so it's easier to understand.
- sitkack 15y agoSee http://vimeo.com/22606387 http://vimeo.com/22606387 Kostis Sagonas goes over PropEr and Dialyzer for Erlang. http://groups.google.com/group/erlang-programming/browse_thread/thread/4e0d1879e271232d http://groups.google.com/group/erlang-programming/browse_thr... http://dialyzer.softlab.ntua.gr/ http://dialyzer.softlab.ntua.gr/ With these two tools one can have a stronger type system than Haskell. PropEr is amazing work. Not to mention CED https://github.com/mariachris/CED https://github.com/mariachris/CED which checks all possible state transitions for race conditions.
- swannodette 15y agoYes, Dialyzer is quite cool. However it is run as a separate tool on your Erlang source right? What I'm aiming for is something that can be used interactively while at the REPL - Qi/Shen is the inspiration here.