Clojurians Log v2

Ohhh this is super super useful, thank you! I like the metadata approach and respect the goal of stripping it out of the runtime. I think that's a really good thing to aim for.

Ah hah! It type checks! Not sure if this is "good" typed clojure code though! Would love feedback if you get a chance but no pressure 🙂

(t/defalias TypedClojureExInfoData
  (t/HMap
   :mandatory {:form t/Any
               :type-error t/Keyword
               :env (t/HMap
                     :mandatory {:line t/Num
                                 :column t/Num
                                 :file t/Str})}))

(t/defalias TypeError
  (t/U
   TypedClojureExInfoData
   (t/HMap
    :mandatory {:message (t/Nilable t/Str)})))

(t/ann ExceptionInfo->type-errors [t/ExInfo :-> (t/ASeq TypeError)])
(defn ExceptionInfo->type-errors
  "Takes an ExceptionInfo from Typed Clojure and converts it to a sequence of maps we can easily display."
  [exinf]
  (let [errors ^{::t/unsafe-cast (t/Seqable t/ExInfo)} (:errors (ex-data exinf))]
    (map
     (fn [error]
       (let [data ^{::t/unsafe-cast TypedClojureExInfoData} (ex-data error)
             {:keys [env form type-error]} data
             {:keys [line column file]} env]
         {:message (ex-message error)
          :form form
          :type-error type-error
          :env {:line line
                :column column
                :file file}}))
     errors)))

Being able to union HMaps makes my brain happy.

I do have to put the metadata on the map I'm pulling from though, not on the symbol I'm binding to, it doesn't like that.

Good to know, adding to the binding should definitely be supported. (probably a bug)

Yes unioned HMaps are a great match for how Clojure is used.

The code you wrote is fine. I might add a couple of cheap assertions like (assert type-error) just to compensate for the unsafe casts.

I think you want t/Merge instead of t/U for TypeError.

Right now, the :message key can probably be any type (try it). t/HMap is open by default, and the checker will pick one element of the union to check the output against. It might be worse actually, you could probably output {:message "string" :form "junk" :type-error "junk" :env "junk"} and because that's technically a '{:message t/Str} (HMap's are open by default), I think that would type check.

Ah understood, that makes a lot of sense. I was also wondering if using malli at runtime to read in things from the outside world or ExData would work well. So malli would runtime type check the values and (I think?) typed clojure can use those malli schemas to understand what the data looks like. Maybe that's the motivation behind the malli integration?

Thank you very much for all of the advice, I'll try to spread this knowledge to others 🙂

I am trying to type check my type checker, it's not really required but I thought it'd be a nice dog food test and a good learning exercise for the type system. I might have to give up on this part though and just move onto to trying to get my PoC working end to end. I've lost a few hours to this already 😬 Translating between the untyped world of Map Any Any to something known seems a bit tricky. Is the canonical way to do that asserts at runtime?

Oh and I define TypeError as

(t/defalias TypeError
  (t/HMap
   :mandatory {:message (t/Nilable t/Str)
               :form t/Any
               :type-error t/Keyword
               :env (t/HMap
                     :mandatory {:line t/Num
                                 :column t/Num
                                 :file t/Str})}))

I guess a big issue is that I'm struggling to read the output like:

Cannot instantiate non-polymorphic type: (t/I [t/Nothing :-> t/Nothing :filters {:then ff, :else ff}] Fn)

...

│ Polymorphic function map could not be applied to arguments:
│ Polymorphic Variables:
│       c
│       a
│       b :..
│
│ Domains:
│       [a b :.. b :-> c] (t/NonEmptySeqable a) (t/NonEmptySeqable b) :.. b
│       [a b :.. b :-> c] (t/Seqable a) (t/Seqable b) :.. b
│
│ Arguments:
│       t/TCError t/Any
│
│ Ranges:
│       (t/NonEmptyASeq c)
│       (t/ASeq c)
│
│ with expected type:
│       (t/Seqable background-check.runner/TypeError)

Especially this part:

│ Arguments:
│       (t/I [t/Nothing :-> t/Nothing :filters {:then ff, :else ff}] Fn) t/Any

t/I is an intersection type.

(t/doc-clj t/I) should give a little more information, and that works for lots of syntax.

I think I wrote a few tutorials about how to read the (admittedly bad) error messages. Here's one that seems serviceable https://stackoverflow.com/a/21682976

In this case, the problem is:

Arguments:
   <...> t/Any

Domains:
   <...> (t/NonEmptySeqable a) <...>
   <...> (t/Seqable a)         <...>

There's no one golden walkthrough. Every time I sit down to do that, I get cold feet and want to change things.

Or the state of things is just too unusable to want to encourage people to use it yet.

Ohh thank you! I didn't realise that was a valid symbol at the REPL, this is a very teach a man to fish moment. Thanks! I think I tried to find that in the docs and it wasn't there and I feel like it wasn't in my autocomplete which is probably user error.

And I get what you mean, it's all good, I'll keep pushing through and learning then try to share what I find.

Thanks for the tips!

So I guess my question now is do you have one more fishing tip around mapping unknown structures into the type system? In this case, ex-data from within an exception? It reminds me of when you try to ingest JSON into a strong type system, you need to somehow safely read it in from an unknown blob into something known at runtime. Is there a special function for this or should I rely on assert to create runtime guarantees that the type checker can lean on? Because this is a real runtime issue, right? I don't know what kind of ex-data I'm going to get out really, so I need the runtime code to robustly check that and bail early while also teaching the type checker about the data that can possibly flow through.

I think this'll be a SUPER common problem for me with types + Clojure, it's just the nature of the beast. So I better get good at it fast 😄

I feel like cast is what I want? So that it'll runtime error if it can't cast. Although maybe things like the typed let will be enough.

Although I've found the typed let / fn blocks cause clj-kondo to have a bad time. Maybe that's something I can configure myself out of but I might lean towards more assert based syntax for now and annotate at the function boundaries instead.

t/I isn't autocompletable since no Typed Clojure types or primitives are backed by vars (any more). used to work, but I removed it. It definitely has a hit on usability, but it helps towards the goal of completely removing Typed Clojure at deployment. Maybe e.g., conjure could scan for ^:typed.clojure metadata and activate t/doc-clj as a fallback for K? Or even we could just alter-var-root clojure.repl/doc to have the same logic if (-> *ns* meta :typed.clojure) . That would work seamlessly with all tooling.

In terms of runtime assertions, there's clojure.core.typed/pred which generates a predicate for a type that you can use for assertions. clojure.core.typed/cast is similar but it's can wrap the output, which has performance implications. https://github.com/typedclojure/typedclojure/tree/main/typed/malli#validation: typed.malli/validate generates a malli validator based on a Typed Clojure type. I thought I implemented malli.core/validate awareness but I can't find it. You can also just https://github.com/typedclojure/typedclojure/blob/0b3ffb01b6a943bdfe0c279cfc7aae78304bec7c/typed/clj.checker/src/typed/cljc/doc.clj#L277-L294 with metadata. ^{::t/unsafe-cast T} E For debugging, the ^::t/dbg E idiom is helpful. best to wrap E in a (do) if it's a macro or not IMeta. You can stack them like ^::t/dbg ^::t/ignore ^{::t/unsafe-cast T} E which prints the resulting type, tells the type checker to not even attempt to check E, then unsafely assigns the result as type T.

The typed macros are basically the old style to me. You shouldn't need to t/let. Instead use:

(let [^{::t/- T} B E])

This works for any macro that binds variables. See the doc-clj docs about ::t/-.

The ideal I'm shooting for is being able to completely strip out all Typed Clojure jars at deployment. So I'm optimizing for being able to just (:require [typed.clojure :as-alias t]).

I have some ideas on how to reliably sweeten the syntax to (let [^{:- T} B E]) but for now it's ugly but has no runtime deps.

Maybe it should be the default now that we opt-in namespaces to being typed.

the problem is if a macro adds :- metadata, we don't want to parse it as a type unless we're completely sure it's intended as a typed op.