Partially applied type in Proxy with Row Type param

Help
#1

I have a function that takes a Proxy for a given open Row Type, and a record of that row type and another one not in the proxy. I’ve gotten it so the function type checks, but now I can’t get the actual Proxy value to type check due to “Type synonym Point is partially applied”.

I am very new to Purescript and have no clue why that would be a problem, let alone how to find the proper way of doing it. Here’s the stripped down code I’m failing with. I want to keep the Proxy there so I can switch it out to a custom data type with even more phantom params that also get used by myFn.

type Named r = (name :: String | r)

type Point r = (x :: Number, y :: Number | r)

myFn :: forall r. Proxy r -> {| r + Named + ()} -> Unit
myFn _ _ = unit

myProxy :: Proxy Point -- Uh oh, why do I have to apply this?
myProxy = Proxy

myTest :: Unit
myTest = myFn myProxy {name: "Vatqihema", x: 10.0, y: 15.0}
#2

Welcome!

PureScript’s type system builds types out of a few building blocks: type application, data and newtype constructors, forall quantification, class constraints, and rows. Type synonyms are not in this list! A type synonym only aliases another type; it doesn’t create a new type.

If this analogy helps, type synonyms are to data types as macros (in some other language with macros!) usually are to functions—they look the same but they don’t represent types/values that you can bind to variables all by themselves. They’re intended to expand early in the type-checking process and then vanish. So you can’t do the things you want to do with Point, because Point is not a type-level function (PureScript doesn’t have first-class type-level functions, although as with Haskell, you can approximate them with classes). It has no meaning if it isn’t applied to another type and then expanded.

If you want to abstract over rows in this way, instead of using the open row pattern (an ‘open row’ is not really a type—it’s just a particular application of type synonyms, and type synonyms don’t create types), you should instead look into the type classes in the Prim.Row built-in module. You can use Union to combine two (closed) row types into another, and unlike type synonyms, row types are actual types in PureScript’s type system; you can abstract over them with forall and pass them around in Proxy and so forth.

1 Like
#3

Oh, that makes more sense. Although I’m still misunderstanding a lot, this was my next iteration on it, which worked!

type Named r = (name :: String | r)

type Point = (x :: Number, y :: Number)

myFn :: forall r1. Proxy r1 -> {|Named r1} -> String
myFn _ myRec = myRec.name

myProxy :: Proxy Point
myProxy = Proxy

myTest :: String
myTest = myFn myProxy {name: "Vatqihema", x: 10.0, y: 15.0}

However, when I tried using a Union or Nub with it, the type signature checked but the myRec var couldn’t access the fields.

myFn2 :: forall r1 r2. Nub (Named r1) r2 => Proxy r1 -> {|r2} -> String
myFn2 _ myRec = myRec.name

myFn3 :: forall r1 r2. Union (Named r1) (other :: Int) r2 => Proxy r1 -> {|r2} -> String
myFn3 _ myRec = myRec.name

I’m still stuck on this and not sure what the issue is. The error is this, which is confusing since I’m not used to the number suffix on type params when I’m not using some nested values or signatures.

  Could not match type
    r21
  with type
    ( name :: String
    | t0
    )
#4

Let’s unpack that error message:

You’ve told the compiler that myRec has type Record r2 (which is what {| r2 } is sugar for). r2 is a quantification variable, so the compiler doesn’t know what concrete type it stands for. So it makes up a new type that it doesn’t know anything about and calls it r21 (it’s just tacking a 1 onto the name you’ve given the variable).

The compiler knows that, in any x.name expression, it needs to match the type of x against Record (name :: a | b) for some arbitrary a and b. So it’s trying to unify those two types: Record r21 and Record (name :: a | b) will unify if r21 unifies with (name :: a | b). But the compiler explicitly doesn’t know anything about r21, so this unification fails, and you get the above error (with a and b having been partially solved by other unifications, in this case).

Now, you’ve told the compiler something about r2—namely, that it appears in a Union or Nub constraint. Unfortunately, while this is enough for a human to work out that there should be a name entry in that row, the compiler doesn’t work backwards through those constraints to figure this out. This has been requested as a feature in Union constraint to add label to row doesn't work · Issue #3242 · purescript/purescript · GitHub, but I don’t think anyone currently has plans to implement it.

Instead, what you can do is replace r2 with something that has the information the compiler is asking for:

myFn3 :: forall r1 r2. Union (Named r1) (other :: Int) (Named r2) => Proxy r1 -> {|Named r2} -> String
myFn3 _ myRec = myRec.name

Now the compiler is still in the dark about what r2 is inside myFn3, but as long as the caller of myFn3 provides enough context for r1 and r2 to be determined, and if those types allow the Union constraint to be solved, everything will check.

2 Likes