Purescript Types Do Not Unify

Question

I have defined a couple of types in my Purescript file:

data Point = Point {
  x :: Int,
  y :: Int
}

data Rect = Rect {
  upperLeft :: Point,
  upperRight :: Point,
  lowerLeft :: Point,
  lowerRight :: Point
}

Now I would like to define a function to check whether two rectangles overlap:

rectsOverlap :: Rect -> Rect -> Boolean
rectsOverlap r s = (r.upperLeft.x > s.lowerRight.x && r.upperLeft.y > s.lowerRight.y)
  || (r.upperLeft.x < s.lowerRight.x && r.upperLeft.y < s.lowerRight.y)
  || (r.lowerLeft.x > s.upperRight.x && r.lowerLeft.y > s.upperRight.y)
  || (r.lowerLeft.x < s.upperRight.x && r.lowerLeft.y < s.upperRight.y)

However, this results in the following error:

  Could not match type

    { upperLeft :: { x :: t0
                   | t1     
                   }        
    | t2                    
    }                       

  with type

    Rect


while checking that type Rect
  is at least as general as type { upperLeft :: { x :: t0
                                                | t1     
                                                }        
                                 | t2                    
                                 }                       
while checking that expression r
  has type { upperLeft :: { x :: t0
                          | t1     
                          }        
           | t2                    
           }                       
while checking type of property accessor r.upperLeft
while checking type of property accessor (r.upperLeft).x
in value declaration rectsOverlap

where t0 is an unknown type
      t1 is an unknown type
      t2 is an unknown type

From what I understand from this message, the compiler is inferring some kind of union type where x is t0 | t1, and upperLeft could also have type t2. When I remove my type annotation the compiler infers the following type for this function:

rectsOverlap :: forall t45 t49 t52 t59 t72 t76 t81 t85 t87 t94.
  Ord t52 => Ord t59 => Ord t59 => Ord t87 => Ord t94 => Ord t87 => Ord t94 => { upperLeft :: { x :: t52
                                                                                              , y :: t59
                                                                                              | t45
                                                                                              }
                                                                               , lowerLeft :: { x :: t87
                                                                                              , y :: t94
                                                                                              | t81
                                                                                              }
                                                                               | t72
                                                                               }
                                                                               -> { lowerRight :: { x :: t52
                                                                                                  , y :: t59
                                                                                                  | t49
                                                                                                  }
                                                                                  , upperRight :: { x :: t87
                                                                                                  , y :: t94
                                                                                                  | t85
                                                                                                  }
                                                                                  | t76
                                                                                  }
                                                                                  -> Boolean

So apparently it's inferring a more general type than my Rect type. But I only want a narrowly defined function. If anyone could shed some light on what is going on here, I would really appreciate it.

Well written question.

devdanke
– devdanke

2022-04-09 12:40:03 +00:00
Commented Apr 9, 2022 at 12:40 — devdanke
– devdanke, Commented Apr 9, 2022 at 12:40

Fyodor Soikin · Accepted Answer · 2019-11-05 04:31:10Z

Records in PureScript are not the same as records in Haskell.

Haskell doesn't have real records as they are understood in most other languages. Haskell's records are just a way to define accessor functions for ADT fields. For example the following two types are almost equivalent:

data A = A Int String
data B = B { x :: Int, y :: String }

Except that type B comes with predefined accessor functions x :: B -> Int and y :: B -> String.

PureScript, on the other hand, has real, ad-hoc, polymorphic, extensible records that are a thing onto themselves. A record in PureScript is defined like this:

{ x :: Int, y :: String }

That's right, there is no need for data or anything. Record are just ad-hoc, sort of like tuples in Haskell. For example:

getX :: { x :: Int, y :: String } -> Int
getX r = r.x

Of course, if you like, you can declare an alias for your record, just like you can do with any other type:

type XY = { x :: Int, y :: String }

getX :: XY -> Int
getX = r.x

You can also use a record as a member of an ADT - again, just like any other type:

data XYWrapped = XYWrapped { x :: Int, y :: String }

But if you do that, you'd need to unwrap the ADT via pattern matching in order to get the record. Again, just like with any other type:

getXWrapped :: XYWrapped -> Int
getXWrapped (XYWrapped r) = r.x

You're not limited to wrapping just one record either (you guessed it: just like with any other type):

data XYPQ = XYPQ { x :: Int, y :: String } { p :: Char, q :: Int }

getXPlusQ :: XYPQ -> Int
getXPlusQ (XYPQ a b) = a.x + b.q

Armed with this knowledge, you can now see that your types Point and Rect are not, in fact, records, but rather ADTs that wrap a single record (and because of this they should be newtypes).

This is why you're getting type mismatch. Because you wrote r.upperLeft, the compiler has inferred that r must be a record that contains a field named upperLeft, but your type signature says that r is of type Rect, which is not a record at all. So the compiler complains.

To fix this, you can either redefine your types as actual records:

type Point = {
  x :: Int,
  y :: Int
}

type Rect = {
  upperLeft :: Point,
  upperRight :: Point,
  lowerLeft :: Point,
  lowerRight :: Point
}

Or you can have your function unwrap the ADTs:

rectsOverlap (Rect r) (Rect s) = 
    let (Point rUpperRight) = r.upperRight
        (Point rUpperLeft) = r.upperLeft
    ....

which would be kinda tedious. So I'd stick with the first option.

Note also that, as mentioned above, PureScript records can be polymorphic and extensible through polymorphism. For more on this, see this answer.

Thank you! That makes sense. Just to clarify, I believe there is a small typo in your code. I think the record definition for point should be: type Point = { x :: Int, y :: Int } Otherwise it causes the following error: A cycle appears in the definition of type synonym Point Cycles are disallowed because they can lead to loops in the type checker. Consider using a 'newtype' instead. Just wanted to clarify. Again, I really appreciate the help.

Collectives™ on Stack Overflow

Purescript Types Do Not Unify

1 Answer 1

1 Comment

Your Answer

Linked

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

1 Comment

Your Answer

Sign up or log in

Post as a guest

Linked

Related