[FRIAM] talk about rabbit holes ...

[Marcus Daniels]

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 <friam-bounces at redfish.com> on behalf of Jon Zingale <jonzingale at gmail.com>
Reply-To: The Friday Morning Applied Complexity Coffee Group <friam at redfish.com>
Date: Friday, March 27, 2020 at 9:46 AM
To: "friam at redfish.com" <friam at 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 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://redfish.com/pipermail/friam_redfish.com/attachments/20200327/d96d949c/attachment.html>