solomonb

Waiting for the remaining broadcast equipment for my LPFM (www.kpbj.fm) to arrive! Then we finally get on the broadcast band. We have over 80 shows at this point. We still need fundraising support. If you are in Los Angeles and want to support freeform community please reach out.

Now I want a hat with the Agnostic Front logo but that says Pareto Front.

I agree that Lean or any of the other languages I listed would be a better choice then Idris and despite how I wrote my original post I wouldn't recommend Idris to someone who explicitly wanted a theorem prover.

Idris has pi and sigma types, dependent pattern matching, view patterns, totality checking, proof search, interactive case splitting, etc, etc.

It is orders of magnitude better then Haskell where the best you can do is hacky bullshit with singletons, GADTs, and type families.

Correct. There are awful tricks to write [1] dependent Haskell but even then it isn't powerful enough and has a significantly worse user experience then a proper dependently typed proof checker (as bad as the UX is on those!).

That said there are other languages such as Agda, Idris, and Rocq that would be fantastic replacements to Lean, especially if you care about staying constructive.

1. https://homepages.inf.ed.ac.uk/slindley/papers/hasochism.pdf

I find that claude rarely uses its memories.

My experience talking with high level mathematicians is that they tend to know their subjects so well and are so excited to share it that they can and will scale their explanation to match their audience.

Thank you for creating Recurse! I had an incredible experience at RC in 2019. I still have friends from my batch.

I deeply wish I had time to do it again.

They offer recruiting services.

I'm reading The Drowned World right now. Incredible book, highly recommended.

To be fair the original commenter was incredibly snarky.

The integer `1` can mean whatever you want, it doesn't need to be a cent. Haskell's `Fixed` type is a good example of this:

https://hackage-content.haskell.org/package/base-4.22.0.0/do...

Its a wrapper around an `Integer` where you declare the scale in the type. So if you use `Fixed E2` as your type then `MkFixed 1` is 1 cent. If you did `Fixed E3` as your type then `MkFixed 1` is 0.1 cent. In both cases it is entirely an integer encoding.

Getting to discover Oleg Kiselyov's work for the first time is such a treat. His web archive is incredible! I'm envious of the author and anyone else discovering it today.

https://okmij.org/ftp/

There was another project I saw years ago that this reminds me of. It was a guy who had been running a simulated city/community for like 20 years. The whole thing was done on pen and paper and used complex rule system he had devised. Similar pre-internet outsider art vibe.

The modern equivalant is the all-in-one karaoke machine :)

The current tenants will see the listing for the vacant unit.

You're absolutely right!

They don't make them like they used to

Messing around with my Lambda Calculus tutorial repo. I just did a total rewrite of Nominal Inductive Types.

https://github.com/solomon-b/lambda-calculus-hs

Interesting! The rules for AM carrier current appear to be more similar to the FM rules, that is they are based on field strength readings that result in a roughly 200ft range.

There is probably a bunch of subtlety about where you measure from as your antenna could be quite large.

To my knowledge there is no legal way to do unlicensed carrier current transmission. Do you have information otherwise? I've always wanted to try it..

The Part15 regulations for AM and FM are more subtle then what you present here. On FM it is based on field strength readings, the exact values of which escape me, but yielding roughly the range you describe.

For AM the rules are more interesting. You can have up to a 3m antenna length and 100mW of DC power input to the final stage of amplification. The optimal setup is a class E amplifier with ~95-99% efficiency into a properly grounded 3m base loaded vertical antenna. The antenna will be grossly undersized but you try to compensate with a huge loading coil. In ideal conditions this setup can get you about 0.5km range.

LPFM is a much more significant undertaking and it is not trivial to get an LPFM license. I know because I have one :)

I run a LPFM radio station here in Los Angeles.

https://www.kpbj.fm/

There are many more LFPMs out there too!

You could take it to the next level and build a part 15 compliant FM transmitter kit.

I respect you for taking the time to review this codebase. Personally I don't want to do that. It sounds like a mess.

Personally I don't want to read the codebase AND book of someone 3 weeks into a mania focused on a subject it is unclear they have any prior experience with. Its disrespectful for someone to think they can produce something worthy of consuming another human's time under those constraints.

As someone genuinely interested in programming language design, type theory, and category theory this sort of thing really saddens me. There is so much passion and rigor that has gone into developing these fields. Chucking all their jargon into an ai slop blender, imo, is actually incredibly disrespectful to those who have worked so hard.

Imagine someone honestly interested in learning about category theory but not yet knowing where to start. Projects like this only serve to muddy the waters obscuring paths to actual learning and giving the impression that the subject is a joke.

How does `refl` work if its not even dependently typed?

Well first of all I think there is more implicit data encoded in the symbols of the epsilon delta definition of limits. In the Mealy example they really just labels for arbitrary sets. The LLM actually failed a much simpler relabeling exercise. Setting that aside, I still think the analogy is flawed.

The student is mid learning process and its entirely reasonable for them one to be relying on pattern recognition until they have fully internalized the subject. The model is fully trained and should thus have internalized their understanding of the subject.

Additionally the student can update their understanding when pattern recognition fails. The model is fully cooked and will never do more then pattern recognition.

I gave chatgpt 3.5 the type signature for a co-algebraic encoding of a mealy machine:

    newtype Mealy s i o = Mealy { runMealy :: (s, i) -> (s, o) }

And it gave a really impressive analysis.

Then I scrambled all the names and asked with a fresh context like:

    newtype Foo z e g = Bar { blob :: (z, e) -> (z, g) }

It got completely confused and generated a bunch of non-sense. It was at that moment I realized that LLMs don't really understand anything.

And yes I understand that a newer model would not get confused by this.

Its amazing that after years of advocating for a materialist view of the mind, the tech bros are flipping to mind-body dualism now that they need to believe a concious mind can exist no body at all.