This page is not created by, affiliated with, or supported by Slack Technologies, Inc.
2023-03-25
Channels
- # announcements (2)
- # beginners (30)
- # biff (12)
- # calva (2)
- # cider (62)
- # clerk (18)
- # clj-commons (20)
- # clojure (9)
- # clojure-europe (6)
- # clojure-switzerland (1)
- # core-logic (6)
- # datomic (4)
- # events (3)
- # fulcro (1)
- # membrane (15)
- # off-topic (16)
- # portal (24)
- # practicalli (2)
- # releases (1)
- # rewrite-clj (45)
- # shadow-cljs (14)
- # tools-build (1)
- # xtdb (4)
I'm working on typeclass resolution ala Haskell. I'm using clojure.core.logic.pldb
as a store of known instances and am able to resolve both instances for simple types (such as Integer
) and parametric ones (such as Option Integer
). However, I cannot resolve more complicated instances such as Option (Option Integer)
. I believe this is because of how I'm modelling the parameter with an lvar
(see comment [1]). From reading chapter 10 of https://scholarworks.iu.edu/dspace/bitstream/handle/2022/8777/Byrd_indiana_0093A_10344.pdf, it seems like nominal logic provides a way of dealing with universally quantified statements, but I'm not sure of how to incorporate this into my solution.
(ns lang.typeclass2
(:refer-clojure :exclude [type ==])
(:require [clojure.core.logic :refer :all]
[clojure.core.logic.pldb :as pldb]))
(pldb/db-rel type t)
(pldb/db-rel typeclass tc)
(pldb/db-rel instance tc t c)
(def db
(pldb/db
[type 'String]
[type 'Integer]
[type 'Function]
[type `(~'Option ~(lvar))]
[typeclass 'Show]
[typeclass 'Eq]
(let [v (lvar)]
[instance 'Show `(~'Option ~v) ;; [1]
[`(~'Show ~v)]])
(let [v (lvar)]
[instance 'Eq `(~'Option ~v)
[`(~'Eq ~v)]])
[instance 'Show 'Integer []]
[instance 'Show 'String []]
[instance 'Eq 'Integer []]
[instance 'Eq 'String []]))
(declare instanceo)
(defne subinstanceso
[scs i]
([[[stc st] . mscs] _]
(fresh [sih sit]
(instanceo stc st sih)
(subinstanceso mscs sit)
(conso sih sit i)))
([[] _]
(== i nil)))
(defn instanceo
[tc t i]
(fresh [scs ih it]
(type t)
(typeclass tc)
(instance tc t scs)
(subinstanceso scs it)
(== ih [tc t])
(conso ih it i)))
(run-db* db [q] (fresh [tc t] (instanceo tc t q)))
(run-db* db [q] (instanceo 'Show '(Option Integer) q))
;; => (([Show (Option Integer)] ([Show Integer])))
(run-db* db [q] (instanceo 'Show '(Option (Option Integer)) q))
;; => ()
Also, general advice on how to improve this code is appreciated as well, I suspect I may be reinventing the wheel in subinstanceso
The issue here is that you have one lvar as the arg to option, and once that is bound it cannot be bound again, you need it to be a fresh lvar for every check
I don't know how to structure it off hand, and am away from my repl, but Option isn't properly a type, it is a type function
The way to do it is to have an Option relation that builds an option type (and I guess adds it to the db, never used pldb much, not clear) and then another relation that derives Show for the option
https://github.com/clojure/core.logic/blob/master/src/main/clojure/clojure/core/logic/nominal.clj core.logic does have some kind of nominal extension