On February 10, 2015 17:44:54 Dan Doel wrote:
> Really, I think the least ad-hoc solution (other than a hypothetical
> best-of-both-worlds inference algorithm) would be to allow code like:
>
> runST do ...
>
> where you can apply expressions directly to certain syntactic constructs
> without
On February 10, 2015 16:28:56 Dan Doel wrote:
> Impredicativity, with regard to type theories, generally refers to types
> being able to quantify over the collection of types that they are then a
> part of. So, the judgment:
>
> (forall (a :: *). a -> a) :: *
>
> is impredicative, because we
I came across something that seems a bit strange to me. Here is a simplified
version (the original was trying to move from a lens ReifiedFold to a
lens-action ReifiedMonadicFold)
{-# LANGUAGE RankNTypes #-}
import Control.Applicative
newtype Wrap = Wrap { extract :: forall f. Functor f =>
