purescript / purescript-typelevel-prelude

Types and kinds for basic type-level programming
BSD 3-Clause "New" or "Revised" License
63 stars 21 forks source link

Add `TypeTypeApply` and `TypeRowApply` aliases? #52

Closed JordanMartinez closed 5 years ago

JordanMartinez commented 5 years ago

Not sure whether this should be discussed/go here, but I'm raising it here since this package already has RowApply.

By using open row types, we can reuse them in various places.

type MyRow r = (name :: String | r)
type OtherRow r = (age :: Int | r)
type FinalRow = (foo :: bar)

f :: { | MyRow + OtherRow + FinalRow }

g :: { | MyRow + () }

h :: SomeTypeTaking (MyRow + ())

The h case (I believe) requires us to wrap the expression in parenthesis. I don't think we can write this as SomeTypeTaking MyRow + ()

Since we already use $ to replace the usage of value-level parenthesis...

f :: Array String -> String
f x = fold $ [ "foo" ] <|> xs

... why not do the same for type-level parenthesis? If so, we could rewrite things like this:

before :: Array (Array (Array String))
after :: Array $ Array $ Array String

With this as a backdrop, it would be ideal if we could use the same idea for applying a row of types to a type constructor

data SomeType (a :: # Type) = -- implementation

foo :: SomeType $ MyRow + OtherRow + ()

However, $ cannot apply a row of types to a type constructor. Doing so will produce a compiler error because the kinds do not match. We cannot currently redefine it to account for multiple kinds because we don't yet have polymorphic kinds. So, perhaps we define a separate type alias for handling this and use the similar infix of $$ to do the same thing?

If so, we could then define both as

type TypeTypeApply f a = f a
infixr 0 type TypeTypeApply as $

example1 :: Array $ Array $ Array String

type TypeRowApply f (a :: # Type) = f a
infixr 0 type TypeRowApply as $$

example2 :: SomeType $ AnotherType $$ MyRow + OtherRow + FinalRow

Note: I'm not sure about the precedence levels. They were taken from @MonoidMusician when he answered my question on the FP Slack.

hdgarrood commented 5 years ago

We could do this, and this library would probably be the place to put them if we were going to do so, but I think I'd rather not. In particular, since we don't have polykinds, as you've pointed out, we'll need one separate operator per kind, which I think makes this a fair bit more awkward than just using parentheses. I personally would rather we not encourage using $ instead of parentheses at the type level at all, even if we did have polykinds, because I'm not really convinced it's an improvement; but then again I'm not a huge fan of $ at the value level either so perhaps that's unsurprising.

JordanMartinez commented 5 years ago

Nate expressed similar reservations due to the polykind issue. Another way this could be resolved is if I define these types myself and use them in my own personal projects. I think that makes the most sense here, so I'll close this issue.

I'm not a huge fan of $ at the value level either so perhaps that's unsurprising.

Care to explain why?

hdgarrood commented 5 years ago

I tend to use $ less often than the average PureScript user because I think parentheses are often more appropriate; everyone understands them, text editors can highlight matching ones, they tend to be a little less confusing in more complex expressions with other operators in play (especially if those other operators have the same precedence as $, although admittedly not very many do).

JordanMartinez commented 5 years ago

Makes sense. Thanks for sharing.