In 3474 I was having trouble defining an existential type as follows:
class C a where
f :: a -> Unit
data Any = Any (forall a. C a => a)
instance anyC :: C Any where
f (Any a) = f a -- (1)
This gives a compiler error. Then, Liam remarked the following:
The type forall a . C a => a means that a user of a term of this type gets to pick which a they want. Which is why Any 3 doesn’t make any sense: you “the implementer” can’t pick the a to be Int if the caller must pick it.
However, I have doubts about this, because with existentials the notion of “user” is a bit more nuanced. Namely, I would expect that a concrete acan be picked when introducing Any and cannot when eliminating. That is, Any 3 should be OK (given an instance C Int) and f above should only know that there is an instance C a and no more. The above program is perfectly fine in Haskell, modulo syntax, so I suspect that forall inside constructors works differently in PureScript?
Does the Haskell code you’re referring to look like data Any = forall a. C a => Any a? (with the forallbefore the type constructor?) If so, that’s something different – it really is an existential type, but it’s special syntax for that. PS doesn’t support that syntax … Would you agree that forall a. C a => a is an universal type by itself? Then it will operate the same inside a datatype.
The “could not match constrained type with constrainted type” issue is well known. Basically, the compiler can’t decide higher-order polymorphism (aka nested foralls), so it doesn’t even try, which is unfortunate, as even a few simple cases (like this) would be helpful. Most of the time it can be worked around via eta-expansion: (\a -> f a) :: forall a. C a => a (because then the compiler introduces the a variable as a skolem, and then it can choose the inner one to unify with that “chosen” a).
Yes, I am indeed referring to ExistentialQuantification. Thanks for confirming my suspicion that that extension is a bit different than this case. Also, thanks for the explanation about type checking. The error message remains unfortunate though, because “symbolically” it shows a trivial situation…
Most of the time it can be worked around via eta-expansion: (\a -> f a) :: forall a. C a => a (because then the compiler introduces the a variable as a skolem, and then it can choose the inner one to unify with that “chosen” a ).
I dont understand
how to use eta-expansion to help me implement Show instance here
module Test where
import Effect
import Effect.Console
import Prelude
import Data.Foldable
import Data.Show
import Unsafe.Coerce
newtype Showable = Showable (forall a . Show a => a)
mkShowable :: ∀ a. Show a => a -> Showable
mkShowable a = Showable a
instance showShowable :: Show Showable where
-- this doesnt work
show (Showable a) = ((\x -> show x) :: forall x . Show x => x -> String) a
{-
31 show (Showable a) = ((\x -> show x) :: forall x . Show x => x -> String) a
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
No type class instance was found for
Data.Show.Show t0
The instance head contains unknown type variables. Consider adding a type annotation.
while applying a function \$dictShow1 ->
\x ->
(show (...)) x
of type Show t0 => t0 -> String
to argument a
while checking that expression (\x ->
show x
)
a
has type String
in value declaration showShowable
where t0 is an unknown type
-}
-- nor this
-- show (Showable a) = ((\(x :: forall xtype . Show xtype => xtype) -> show x)) a
{-
31 -- show (Showable a) = ((\x -> show x) :: forall x . Show x => x -> String) a
No type class instance was found for
Data.Show.Show t0
The instance head contains unknown type variables. Consider adding a type annotation.
while applying a function \$dictShow2 ->
\x ->
(show (...)) x
of type Show t0 => t0 -> String
to argument a
while checking that expression (\x ->
show x
)
a
has type String
in value declaration showShowable
-}
showables :: Array Showable
showables = [mkShowable 1, mkShowable unit, mkShowable "hello"]
main :: Effect Unit
main = do
log $ intercalate ", " (map show showables)
newtype Showable = Showable (forall r. (forall a. Show a => a -> r) -> r)
mkShowable :: forall a. Show a => a -> Showable
mkShowable a = Showable \k -> k a
unShowable :: forall r. (forall a. Show a => a -> r) -> Showable -> r
unShowable k1 (Showable k2) = k2 k1
test1 = mkShowable 42
test2 = unShowable (\a -> show a) test1
I rewite your pattern in hasekll, but purescript doesn’t support use Constraint from parameter, if purescript support that, we can write generic form, but not a pattern
newtype Exist (k :: Type -> Constraint)
= Exist (forall (r :: Type). (forall (a :: Type). (k a) => a -> r) -> r)
