Showable type - PureScript

Can exists be used to implement a Showable type like what is done here? I don't see how to get the Show constraint.

Nope. purescript-exists uses a direct unsafeCoerce-based representation of the existential, instead of the Church encoding which uses a lambda. The Church encoding could let you pass extra data in the closure of the lambda, but the coercion-based encoding can only represent unconstrained existentials.

so does exists have any advantage over the church encoding method?

Performance, probably?

https://github.com/purescript/purescript-exists/issues/5

huh, one less lambda allocation doesn't seem worth it to me to give up that much power, but :shrug:

Well, switching encodings isn't necessarily enough to get you what you want either.

I don't think the type system lets you express an Exists that is generic over constrained and unconstrained types.

Are you saying you need to implement an ad hoc one whenever you need it?

I think so, until PureScript gets constraint kinds or something.

hm, I kinda assumed that bit in the article that was like

(Question: can we write this using the type Exists from above?)

was included as sort of an exercise to the reader, which made me guess that it was possible somehow, but perhaps it was a legitimate question

and the answer is "no"

Or it's both: an exercise for the reader to which the answer is ‘no’. :big_smile:

What you need to generalize Showable is something like:

newtype ConstrainedExists c = ConstrainedExists (∀ r. (∀ a. c a => a -> r) -> r)

But that c a => isn't legal.

rhendric said:

Or it's both: an exercise for the reader to which the answer is ‘no’. :big_smile:

good point! :big_smile:

rhendric said:

What you need to generalize Showable is something like:

newtype ConstrainedExists c = ConstrainedExists (∀ r. (∀ a. c a => a -> r) -> r)

A bit late to the party. It depends what you want to achieve. If it is passing a dictionary around a la SYTC:

-- hydrate dictionary with whatever...
newtype ConstrainedExists c = ConstrainedExists (∀ r. (∀ a. { show :: a -> String, eq :: a -> a -> Boolean } -> a -> r) -> r)

This strategy can already go quite far - it's possible to handle fixed points, induction, etc.

True, but I'm not sure that's quite in the spirit of the referenced blog post. Explicitly repacking your typeclass dictionary in that way is a decent workaround for not having constraint kinds, but it doesn't offer the ergonomics of passing something that is Show in and getting something that is Show out, at least not without some Show-specific boilerplate comparable to just writing Showable.

-- hydrate dictionary with whatever...
newtype ConstrainedExists c = ConstrainedExists (∀ r. (∀ a. { show :: a -> String, eq :: a -> a -> Boolean } -> a -> r) -> r)

I'm confused about what is going on here. c doesn't appear on the right side at all. At first I thought

newtype ConstrainedExists c = ConstrainedExists (∀ r. (∀ a. c -> a -> r) -> r)

is what was meant, that way you could set up your constraints by setting c, but given that c relies on a, which is inside a higher rank type, I would think you still couldn't give it arbitrary constraints in this way. Is there something I'm missing?

What about

newtype ConstrainedExists c = ConstrainedExists (∀ r. (∀ a. c a -> r) -> r)

You could then pass it something like

type ShowConstraint a = Show a => a

(Idk if that works, cant try it rn)

unknown-33.png

Welp

It helps to mentally replace => with -> (which is what it is at runtime) - Show a -> a is a function from Show instance to a value, but you probably want equivalent of Show a /\ a

Also, you can't partially apply type synonyms, so ConstrainedExists ShowConstraint wouldn't be valid anyway.

This, however, works:

newtype ConstrainedExists c = ConstrainedExists (∀ r. (∀ a. c a r) -> r)

newtype ShowConstraint a r = ShowConstraint (Show a => a -> r)

newtype Hidden = Hidden Int

x :: ConstrainedExists ShowConstraint
x = ConstrainedExists (\(ShowConstraint f) -> f 72)

-- error: No type class instance was found for Data.Show.Show Hidden
--y :: ConstrainedExists ShowConstraint
--y = ConstrainedExists (\(ShowConstraint f) -> f (Hidden 72))

But it doesn't save you from having to make that Show-specific newtype.

why does the above approach work but not @Matei Adriel's :thinking:

@rhendric I used a type synnonim for the Exists type as well

oh, maybe that's why?

Im not sure, imma experiment w it a lite bit more