Rho Calc Grammar in Scala

Rho.scala

object Rho {
// Grammar Definition
  sealed trait P

  case class zero() extends P                    // 0
  case class input( y: X, x: X, p: P ) extends P // for(y <- x) { p }
  case class lift( x: X, q: P ) extends P        // x!(q)
  case class drop( x: X ) extends P              // *x
  case class parallel( p: P, q: P ) extends P    // p | q

  sealed trait X

  case class quote( p: P ) extends X             // @p

  // Some things that I am not happy with:
  //  1: It seems annoying to have to expose the trait X along with the trait P.
  //     When we look at the equational represenation of Rho: P[X] = ... , RP = P[RP],
  //     we don't really expose a second "class" of objects that are names, we just drop processes
  //     into holes that accept names.
  //  2: It would be nice to be able to define rho-calc from the parametric definition of process P[X]
  //     in a more generic way. This seems like it should be possible. I've looked at encoding the SKI
  //     calculus into scala's type system, and taken cursory looks at the scalaz & cats libraries,
  //     but am not quite sure how to know that I'm sniffing down the right path.
  
// Free and Bound Name Definitions
  def FN( p: P ) : Set[X] = {
    p match {
      case zero()           => Set.empty[X]
      case input( y, x, p ) => (FN(p) - y) + x
      case lift( x, p )     => FN(p) + x
      case drop( x )        => Set(x)
      case parallel( p, q ) => FN(p) | FN(q)
    }
  }
  
  def N( p: P ) : Set[X] = {
    p match {
      case zero()           => Set.empty[X]
      case input( y, x, p ) => N(p) + (y, x)
      case lift( x, p )     => N(p) + x
      case drop( x )        => Set(x)
      case parallel( p, q ) => N(p) | N(q)
    }
  }
  
  def BN( p: P ) : Set[X] = {
    N(p) &~ FN(p)
  }
  
}

This is not a functional implementation. I do not check for the structural equality of processes to get to name equality.