[FRIAM] talk about rabbit holes ...

[uǝlƃ ☣]

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 follow-on work for Dependent Haskell.  As far as I can tell it is another one of those drawn-out projects that the Haskell community manages to endure/ignore.
>
> On 3/27/20 9:45 AM, Jon Zingale wrote:
>> 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 project strikes me as being one
>> of bull headedness, a just-to-see-if-one-can kind of thing.
>> 
>> Do you think they will go so far as to implement general dependent
>> typing? Last night at some point, I was thinking about the problem of
>> implementing flexible contravariant functors in a computing language.
>> This often appears to a stumbling block when I set out to define /for all/
>> and /there exists/ from a substitution functor, a la Topos theory.
>> Any thoughts are welcome.

-- 
☣ uǝlƃ