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.
From: Friam <[email protected]> on behalf of Jon Zingale <[email protected]> Reply-To: The Friday Morning Applied Complexity Coffee Group <[email protected]> Date: Friday, March 27, 2020 at 9:46 AM To: "[email protected]" <[email protected]> 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 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. Jon
============================================================ FRIAM Applied Complexity Group listserv Meets Fridays 9a-11:30 at cafe at St. John's College to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com archives back to 2003: http://friam.471366.n2.nabble.com/ FRIAM-COMIC http://friam-comic.blogspot.com/ by Dr. Strangelove
