I have written two tagless algebras and I would like to write the laws for one of them.
The algebras are as follows:
@newtype case class Variable(v: String)
@newtype case class Value(v: String)
trait Environment[F[_]] {
def get(v: Variable): F[Option[Value]]
}
@newtype case class DbUrl(v: String)
@newtype case class DbUser(v: String)
@newtype case class DbPw(v: String)
final case class DbParams(url: DbUrl, user: DbUser, pw: DbPw)
trait DbConnector[F[_]] {
def read(url: DbUrl, user: DbUser, pw: DbPw): F[DbParams]
}
The interpreters are as follows:
object Environment {
def apply[F[_]](implicit ev: Environment[F]): ev.type = ev
def impl[F[_] : Sync]: Environment[F] = new Environment[F] {
override def get(v: Variable): F[Option[Value]] =
Sync[F].delay(sys.env.get(v.v).map(a => Value(a)))
}
}
final case class LiveDbConnector[F[_] : MonadError[*[_], Throwable]](env: Environment[F]) extends DbConnector[F] {
override def read(url: DbUrl, user: DbUser, pw: DbPw): F[DbParams] =
(for {
a <- OptionT(env.get(Variable(url.v)))
b <- OptionT(env.get(Variable(user.v)))
c <- OptionT(env.get(Variable(pw.v)))
} yield DbParams(DbUrl(a.v), DbUser(b.v), DbPw(c.v)))
.value
.flatMap {
case Some(v) => v.pure[F]
case None => DbSettingError.raiseError[F, DbParams]
}
}
object DbConnector {
def impl[F[_] : MonadError[*[_], Throwable]](env: Environment[F])
: DbConnector[F] =
new LiveDbConnector[F](env)
In the functional programming there are laws such as Monoid, Monads and etc.
My questions are:
DbConnector
algebraYou are confusing mathematical laws and soundness with the correctness of your programs.
Firstly, Monad, Monoid, Fold etc. aren't laws. They are mathematical "structures" that come from Category Theory. These "structures" have certain properties that they need to adhere to, to be sound and correct. One set of these properties, for example, is known as Monadic Laws
Any Monadic structure in mathematics needs to abide by these 3 rules:
The operations on Monad, flatMap and pure (or join and return in mathematics) has to be correct with respect to these laws to function properly. i.e. pure(a).flatMap(f) == f(a)
, M.flatMap(pure) == M
etc.
In functional programming, Monads are a design pattern derived from these mathematical structures and laws. They describe some "composable computation". In cats Monad is defined as a typeclass. This structure adheres to the aforementioned rules.
How should I write laws for DbConnector algebra
If you want to prove laws, you probably would need to use a theorem prover, there is really no way of explicitly writing or testing laws in Scala but you can always write unit tests to make sure your Monad adheres to these law, i.e. testFlatMapLeftIdentity(...)
etc.
Do my algebras need laws or writing the unit tests is enough?
In short, I can not think of a case where an algebra have explicit laws, unless your algebra is describing some mathematical set of operations. For example, in your code the context bound MonadError[*[_], Throwable]]
requires a Monad[F]
in scope, which needs to abide by these laws, assuming your are using the common IO, Task, Future
etc., cats have made it so you don't need to worry about these laws. If you ever decide to implement your own effect type or write a new Monad implementation, you will need to make sure you stick by these laws but there is nothing in your code that requires you to worry about them. Writing good unit tests for this algebra would be enough.