Re: [FRIAM] talk about rabbit holes ...

The Basold paper looks really good, I am excited to jump in. Perhaps as a side note, these are really exciting times. How wonderful to see the places modern type theory is seeping its way into the structure and implementation of practical programs.

Re: [FRIAM] talk about rabbit holes ...

he Mercury programming language. Cross referencing sets like that in Mercury is done in a nice way. Marcus From: Friam on behalf of Jon Zingale Sent: Friday, March 27, 2020 11:46 PM To: friam@redfish.com Subject: [FRIAM] talk about rabbit holes ... Glen, Marcus

[FRIAM] talk about rabbit holes ...

Glen, Marcus, FWIW, I spent the evening sketching out a direction that could be fruitful when writing the quantifiers from the perspective of an adjoint situation. It would be cool if it could be easily extended to doing

Re: [FRIAM] talk about rabbit holes ...

Marcus, Mostly, I bring up the issue of defining the quantifiers via functors for the academic challenge of it, but also thank you for looking up the singletons library. Getting under the hood of that library will likely have some beautiful code and likely a couple of balls-of-mud. Generally, I

Re: [FRIAM] talk about rabbit holes ...

I can't imagine he'd try to extend his "helper functions" that far, no. I wasn't even familiar with Prover9 until I saw that post: https://www.cs.unm.edu/~mccune/mace4/ It's a small world after all. On 3/27/20 10:35 AM, Marcus Daniels wrote: > There’s the singletons library for GHC, and some

Re: [FRIAM] talk about rabbit holes ...

Coffee Group Date: Friday, March 27, 2020 at 9:46 AM To: "friam@redfish.com" Subject: Re: [FRIAM] talk about rabbit holes ... Glen, It is kind of funny to me, and yet should not surprise me, that an individual was motivated to write a theorem prover in R. OTOH, every attempt I have

Re: [FRIAM] talk about rabbit holes ...

Glen, It is kind of funny to me, and yet should not surprise me, that an individual was motivated to write a theorem prover in R. OTOH, every attempt I have ever made to get Agda to work for me has required sandboxing my Haskell environments and switching to an emacs editor, so hey. Still, the

Re: [FRIAM] talk about rabbit holes ...

> Sorry for being unclear. I didn't intend to say that Frank Ramsey, who died > in 1930, was the jerk. It's Jeffrey Ketland that I'm concerned about. I felt that I was parsing that wrong but because I was rather tired and losing focus I rushed to respond without going back and double-checking my

Re: [FRIAM] talk about rabbit holes ...

Sorry for being unclear. I didn't intend to say that Frank Ramsey, who died in 1930, was the jerk. It's Jeffrey Ketland that I'm concerned about. And to be fair, it is traumatic to have an acquaintance commit suicide, regardless of the circumstances. Whether the "social justice league" who

Re: [FRIAM] talk about rabbit holes ...

Glen - Not just any ole rabbit hole but a very convoluted/complex (albeit interesting) one. I dove into your last link (only) because I've been wanting to understand more better what YOUR view of postmoderism is...   on the whole I like what I read.   I don't have the focus nor bandwidth right

[FRIAM] talk about rabbit holes ...

So, I find this: Theorem Proving, Multigraphs and Euler Cycles in R. Part I https://criticathink.wordpress.com/2020/03/21/theorem-proving-multigraphs-and-euler-cycles-in-r-i/ Which is pretty cool. And I think, wow a philosopher who uses R! Maybe I should follow this dude on feedly or somesuch.