Fork me on GitHub
#core-logic
<
2023-03-25
>
jgertm01:03:52

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))
;; => ()

jgertm01:03:38

Also, general advice on how to improve this code is appreciated as well, I suspect I may be reinventing the wheel in subinstanceso

hiredman02:03:21

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

hiredman02:03:10

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

hiredman02:03:42

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