<div dir="ltr"><div></div><div class="markdown-here-wrapper" style><p style="margin:1.2em 0px!important">I recently experimented with that kinda stuff. See the following:</p>
<pre style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;font-size:1em;line-height:1.2em;margin:1.2em 0px"><code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248);white-space:pre;overflow:auto;border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;border:1px solid rgb(204,204,204);padding:0.5em 0.7em;display:block!important;display:block;padding:0.5em;color:rgb(51,51,51);background:rgb(248,248,255)">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
</code></pre><p style="margin:1.2em 0px!important">The above code ensures that transactions of type <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248)">Transaction Read r</code> cannot be executed using the <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248)">executeUpdateTransaction</code> function. However then the same type level logic can be encoded using an existence of a type class instance:</p>
<pre style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;font-size:1em;line-height:1.2em;margin:1.2em 0px"><code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248);white-space:pre;overflow:auto;border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;border:1px solid rgb(204,204,204);padding:0.5em 0.7em;display:block!important;display:block;padding:0.5em;color:rgb(51,51,51);background:rgb(248,248,255)">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
</code></pre><div title="MDH:PGRpdj5JIHRoaW5rIHJlY2VudGx5IGV4cGVyaW1lbnRlZCB3aXRoIHRoYXQga2luZGEgc3R1ZmYu
IFNlZSB0aGUgZm9sbG93aW5nPC9kaXY+PGRpdj48YnI+PC9kaXY+PGRpdj5gYGA8L2Rpdj48ZGl2
PnR5cGUgZmFtaWx5IFNlbGVjdFByaXZpbGVnZSBhIDo6IEJvb2w8L2Rpdj48ZGl2PnR5cGUgaW5z
dGFuY2UgU2VsZWN0UHJpdmlsZWdlIFJlYWRUcmFuc2FjdGlvbiAmbmJzcDs9IFRydWU8L2Rpdj48
ZGl2PnR5cGUgaW5zdGFuY2UgU2VsZWN0UHJpdmlsZWdlIFdyaXRlVHJhbnNhY3Rpb24gPSBUcnVl
PC9kaXY+PGRpdj48YnI+PC9kaXY+PGRpdj50eXBlIGZhbWlseSBVcGRhdGVQcml2aWxlZ2UgYSA6
OiBCb29sPC9kaXY+PGRpdj50eXBlIGluc3RhbmNlIFVwZGF0ZVByaXZpbGVnZSBSZWFkVHJhbnNh
Y3Rpb24gJm5ic3A7PSBGYWxzZTwvZGl2PjxkaXY+dHlwZSBpbnN0YW5jZSBVcGRhdGVQcml2aWxl
Z2UgV3JpdGVUcmFuc2FjdGlvbiA9IFRydWU8L2Rpdj48ZGl2Pjxicj48L2Rpdj48ZGl2PmRhdGEg
UmVhZDwvZGl2PjxkaXY+ZGF0YSBXcml0ZTwvZGl2PjxkaXY+PGJyPjwvZGl2PjxkaXY+ZGF0YSBU
cmFuc2FjdGlvbiB0IHI8L2Rpdj48ZGl2Pjxicj48L2Rpdj48ZGl2PmV4ZWN1dGVVcGRhdGVUcmFu
c2FjdGlvbiA6OiBVcGRhdGVQcml2aWxlZ2UgdCB+IFRydWUgPSZndDsgVHJhbnNhY3Rpb24gdCBy
IC0mZ3Q7IElPIHI8L2Rpdj48ZGl2PmV4ZWN1dGVVcGRhdGVUcmFuc2FjdGlvbiA9PC9kaXY+PGRp
dj4mbmJzcDsgdW5kZWZpbmVkPC9kaXY+PGRpdj7igItgYGA8L2Rpdj48ZGl2Pjxicj48L2Rpdj48
ZGl2PlRoZSBhYm92ZSBjb2RlIGVuc3VyZXMgdGhhdCB0cmFuc2FjdGlvbnMgb2YgdHlwZSBgVHJh
bnNhY3Rpb24gUmVhZCByYCBjYW5ub3QgYmUgZXhlY3V0ZWQgdXNpbmcgdGhlIGBleGVjdXRlVXBk
YXRlVHJhbnNhY3Rpb25gIGZ1bmN0aW9uLiBCdXQgdGhlbiB0aGUgc2FtZSB0eXBlIGxldmVsIGxv
Z2ljIGNhbiBiZSBlbmNvZGVkIHVzaW5nIGFuIGV4aXN0ZW5jZSBvZiBhIHR5cGUgY2xhc3MgaW5z
dGFuY2U6PC9kaXY+PGRpdj48YnI+PC9kaXY+PGRpdj5gYGA8L2Rpdj48ZGl2PmNsYXNzIFNlbGVj
dFByaXZpbGVnZSB0PC9kaXY+PGRpdj5pbnN0YW5jZSBTZWxlY3RQcml2aWxlZ2UgUmVhZFRyYW5z
YWN0aW9uPC9kaXY+PGRpdj5pbnN0YW5jZSBTZWxlY3RQcml2aWxlZ2UgV3JpdGVUcmFuc2FjdGlv
bjwvZGl2PjxkaXY+PGJyPjwvZGl2PjxkaXY+Y2xhc3MgVXBkYXRlUHJpdmlsZWdlIHQ8L2Rpdj48
ZGl2Pmluc3RhbmNlIFVwZGF0ZVByaXZpbGVnZSBXcml0ZVRyYW5zYWN0aW9uPC9kaXY+PGRpdj48
YnI+PC9kaXY+PGRpdj5kYXRhIFJlYWQ8L2Rpdj48ZGl2PmRhdGEgV3JpdGU8L2Rpdj48ZGl2Pjxi
cj48L2Rpdj48ZGl2PmRhdGEgVHJhbnNhY3Rpb24gdCByPC9kaXY+PGRpdj48YnI+PC9kaXY+PGRp
dj5leGVjdXRlVXBkYXRlVHJhbnNhY3Rpb24gOjogVXBkYXRlUHJpdmlsZWdlIHQgPSZndDsgVHJh
bnNhY3Rpb24gdCByIC0mZ3Q7IElPIHI8L2Rpdj48ZGl2PmV4ZWN1dGVVcGRhdGVUcmFuc2FjdGlv
biA9PC9kaXY+PGRpdj4mbmJzcDsgdW5kZWZpbmVkPC9kaXY+PGRpdj5gYGA8L2Rpdj4=" style="height:0;font-size:0em;padding:0;margin:0"></div></div><div></div><div class="gmail_extra"><br><div class="gmail_quote">2014-10-16 14:58 GMT+04:00 Ivan Lazar Miljenovic <span dir="ltr"><<a href="mailto:ivan.miljenovic@gmail.com" target="_blank">ivan.miljenovic@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Using the Constraint type and the ConstraintKinds extension, is there<br>
any way we can determine if a Constraint is satisfied (i.e. a<br>
type-level function of type Constraint -> Bool using DataKinds)?<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
Ivan Lazar Miljenovic<br>
<a href="mailto:Ivan.Miljenovic@gmail.com">Ivan.Miljenovic@gmail.com</a><br>
<a href="http://IvanMiljenovic.wordpress.com" target="_blank">http://IvanMiljenovic.wordpress.com</a><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</font></span></blockquote></div><br></div></div>