RE: Visible Type Applications

[purefunctor]

Description of the change

Closes #3137, closes #4235. An alternative implementation of visible type applications that simplifies the type-checking rules and extraneous features. This PR also depends on #4376.

Like mentioned, this PR simplifies the type-checking rules used for visible type applications, as well as the extraneous features that come with #4235. In particular, the following is true for this implementation:

• @ is still required for making type variables available under type application;
• however, variables in class heads and data declarations are available by default.

IIRC, a few other features that were brought up were:

1. the ability to intersperse regular function application and type applications, similar to as if you had a proxy-based API.
2. the ability to change type variable visibility between type class members.

Though, I feel that:

Personally, I'd say it'd be good to merge this minimal version of type applications to gauge interest in the extra features that was discussed in the first PR. It's mostly an additive change that would offer a concise alternative to proxy-based APIs.

As a reply to @mikesol's

[..] IMO a good place to look is the Haskell community, as they already have VTAs and you can get a good sense if folks are happy with the implementation & what they feel is lacking.

---

Checklist:

• Added a file to CHANGELOG.d for this PR (see CHANGELOG.d/README.md)
• Added myself to CONTRIBUTORS.md (if this is my first contribution)
• Linked any existing issues or proposals that this pull request should close
• Updated or added relevant documentation
• Added a test for the contribution (if applicable)

[artemisSystem]

however, variables in class heads and data declarations are available by default.

Potential future feature: the ability to change type variable visibility between type class members.

Just pointing out that this would be a breaking change, as far as i understand? Not sure if that is a big deal or not, but something to keep in mind.

[purefunctor]

however, variables in class heads and data declarations are available by default.

Potential future feature: the ability to change type variable visibility between type class members.

Just pointing out that this would be a breaking change, as far as i understand? Not sure if that is a big deal or not, but something to keep in mind.

@artemisSystem It depends. The breaking change here would come from the new syntactic forms which determines if a type is available for type application or not. I think that having them on by default for class heads and data declarations is reasonable to allow for usage w/o introducing more friction.

I can also imagine the latter being another additive feature, but I'm just not sure how to achieve that syntactically yet. Maybe, something along the lines of:

class Visibility a where
  visibility :: Invisible a => a -> a
  -- or `visibility :: invisible a. a -> a`?

where Invisible is basically a sentinel just for the compiler to use. If the need to have selective visibility for constructors, how should we go about that?

[MonoidMusician]

I think the errors you added should be unified to a "monomorphic/not-visibly-polymorphic type cannot have a type application". It would be great if those had separate error text based on whether it is polymorphic or not: “cannot type-apply the monomorphic type Int -> Int” and “cannot apply (polymorphic) type without visible quantification: forall a. a -> a”.

I think the current behavior of @_ may be confusing if the expression still being polymorphic is visible to the user in some cases (ahem, record fields?). What happens if we don't special case it? What happens to _ nested in other type expressions? Will have to think about it and test it.

Will take a look at more of the logic later.

[purefunctor]

This error can be expanded further by suggesting that the user can change the signature of the inferred type to allow it to be used in type application.

I think that for polymorphic types, it's the case that they're often written out by the user such that we can suggest editing the source, but I feel we can clarify this in the error index for the documentation page.

[JordanMartinez]

My approval above means it's my opinion that it's better to merge this in its current state now than not to merge it. If it does implement the feature while not handling edge cases or other situations properly, it's not like we don't have other useful language features that have their own years-long-standing edge-case bugs. To me, the net gain of a language feature that mostly works, especially one as highly desired as this one, is better than the possible downsides. Moreover, by getting it merged, it provides feedback on what edge cases this PR may still not yet resolve or other design situations not yet considered.

But, because I know that others are more qualified when it comes to reviewing this part of the codebase, I'm choosing not to merge this at this time despite all our usual constraints being satisfied otherwise. On one hand, I may just be struggling with politician's syllogism, and maybe the real issue to further discuss are design questions not yet answered in the linked issue (of which I can't recall whether there were such issues, nor what those are). On the other hand, I do think that, if no one objects to merging this, that I will merge this sometime in the future.

[JordanMartinez]

It's been a month since my previous comment. Since no one has objected, I'm merging.

[deemp]

It's so cool!

Following #3137 (comment), I used a shorter synonym for prop from purescript-profunctor-lenses.

p :: ∀ @l r1 r2 r a b. IsSymbol l ⇒ Cons l a r r1 ⇒ Cons l b r r2 ⇒ Lens (Record r1) (Record r2) a b
p = prop (Proxy @l)

type St = {someField :: Int }

st :: St
st = { someField : 1}

ip :: Int
ip = view (p @"someField") st

[paluh]

Actually I tried to shorten the function and drop the proxy parameter from prop all together which essentially works:

prop'
  :: forall @l r r1 r2 a b
   . IsSymbol l
  => Row.Cons l a r r1
  => Row.Cons l b r r2
  => Lens { | r1 } { | r2 } a b
prop' = do
  let p = Proxy @l
  lens (Record.get p) (flip (Record.set p))

_test
  :: forall r36 a37 b38 p
   . Strong p
  => p a37 b38
  -> p { test :: a37 | r36 } { test :: b38 | r36 }
_test = prop' @"test"

The problem is that by default compiler derived a type for _test which wasn't correct and caused compile error (so I copied the signature above from the original Lens.Record.prop $ Proxy @"test"). Compiler derived type:

_test
  :: forall r r1 r2 a b
   . IsSymbol "test"
  => Row.Cons "test" a r r1
  => Row.Cons "test" b r r2
  => (forall p. Strong p => p a b -> p (Record r1) (Record r2))

Compiler error:

[1 of 1] Compiling Contrib.Record                   
Error found:                                                                                            
in module Contrib.Record          
at src/Contrib/Record.purs:38:9 - 38:22 (line 38, column 9 - line 38, column 22)                        
                                                    
  Could not match type                                                                                  
                                 
    ( test :: a1                                                                                        
    | t5                                                                                                                                                                                                         
    )                                                                                                   
                                                                                                        
  with type                         
                                                                                                                                                                                                                 
    r13                                        
       
                                                    
while solving type class constraint                                                                     
                                  
  Prim.Row.Cons "test"                                       

I think that this is unexpected behavior. Should I fill in a bug report for that?

[MonoidMusician]

The error you see with that inferred type is already filed as #3243