[Haskell-cafe] Converting a Constraint to Bool

[Nikita Volkov]

I recently experimented with that kinda stuff. See the following:

type family SelectPrivilege a :: Bool
type instance SelectPrivilege ReadTransaction  = True
type instance SelectPrivilege WriteTransaction = True

type family UpdatePrivilege a :: Bool
type instance UpdatePrivilege ReadTransaction  = False
type instance UpdatePrivilege WriteTransaction = True

data Read
data Write

data Transaction t r

executeUpdateTransaction :: UpdatePrivilege t ~ True => Transaction t r -> IO r
executeUpdateTransaction =
  undefined
​

The above code ensures that transactions of type Transaction Read r cannot
be executed using the executeUpdateTransaction function. However then the
same type level logic can be encoded using an existence of a type class
instance:

class SelectPrivilege t
instance SelectPrivilege ReadTransaction
instance SelectPrivilege WriteTransaction

class UpdatePrivilege t
instance UpdatePrivilege WriteTransaction

data Read
data Write

data Transaction t r

executeUpdateTransaction :: UpdatePrivilege t => Transaction t r -> IO r
executeUpdateTransaction =
  undefined

​

2014-10-16 14:58 GMT+04:00 Ivan Lazar Miljenovic <ivan.miljenovic at gmail.com>
:

> Using the Constraint type and the ConstraintKinds extension, is there
> any way we can determine if a Constraint is satisfied (i.e. a
> type-level function of type Constraint -> Bool using DataKinds)?
>
> --
> Ivan Lazar Miljenovic
> Ivan.Miljenovic at gmail.com
> http://IvanMiljenovic.wordpress.com
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141016/0b59b395/attachment.html>