<div dir="ltr">Hi Marc,<div><br></div><div>You can try `doSensitiveThings (Proxy :: Proxy 'Admin)`, recall that we have `data Proxy (a :: k) = Proxy`, it does nothing on value level, but it effectively passes a type (in this case 'Admin) as an argument, I guess that's where the name "Proxy" comes from.</div><div><br></div><div>Cheers,</div><div>Javran</div></div><br><div class="gmail_quote"><div dir="ltr">On Fri, Nov 23, 2018 at 11:59 PM Marc Busqué <<a href="mailto:marc@lamarciana.com">marc@lamarciana.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Thank you very much for this dedicated explanation, Frank.<br>
<br>
With your last example, where you are tagging the `RealUser` type with a<br>
type of `UserKind`, I have come to appreciate the usefulness of<br>
`DataKinds`. And it is really nice.<br>
<br>
However, I still don't understand the example without those final<br>
changes. I copy it again here for more context:<br>
<br>
```<br>
{-# LANGUAGE DataKinds #-}<br>
<br>
import Data.Proxy<br>
<br>
data UserKind = User | Admin<br>
<br>
data RealUser = RealUser { userAdminToken :: Maybe (Proxy 'Admin) }<br>
<br>
doSensitiveThings :: Proxy 'Admin -> IO ()<br>
doSensitiveThings = undefined<br>
```<br>
<br>
How am I supposed to call here `doSensitiveThings`? I need to provide it<br>
a value of type `Proxy 'Admin`, but, as fas as I know, promoted data<br>
constructors (`'Admin` here) are uninhabited.<br>
<br>
Thanks,<br>
<br>
Marc Busqué<br>
<a href="http://waiting-for-dev.github.io/about/" rel="noreferrer" target="_blank">http://waiting-for-dev.github.io/about/</a><br>
<br>
On Mon, 19 Nov 2018, Frank Staals wrote:<br>
<br>
> Marc Busqué <<a href="mailto:marc@lamarciana.com" target="_blank">marc@lamarciana.com</a>> writes:<br>
><br>
>> I'm reading Sandy Maguire book Thinking with Types, and I'm stuck<br>
>> understanding an example about `DataKinds` language extension.<br>
>><br>
>> In the book, it is said that it can be used to prevent at the type level<br>
>> that non admin users perform some action for which admin privileges are<br>
>> required.<br>
>><br>
>> So, in the example, having `DataKinds` enabled, we define:<br>
>><br>
>> ```<br>
>> data UserType = User | Admin<br>
>> ```<br>
>><br>
>> Then, we change User type:<br>
>><br>
>> ```<br>
>> data User = User<br>
>> { userAdminToken :: Maybe (Proxy 'Admin) }<br>
>> ```<br>
>><br>
>> And then it is said that we can enforce that sensitive operations are<br>
>> performed by a user with the admin token:<br>
>><br>
>> ```<br>
>> doSensitiveThings :: Proxy 'Admin -> IO ()<br>
>> ```<br>
>><br>
>> No other language extensions have been explained before in the book, and<br>
>> I simply don't understand how it is works...<br>
>><br>
>> First, I guess that when writing `data User = ...` we are overriding<br>
>> `'User` promoted data constructor. Isn't it?<br>
><br>
> The second 'User' type (and constructor) are both different from the 'User'<br>
> constructor in the UserType type. It may be clearer if we slightly<br>
> rename these types and the constructors a bit to something like:<br>
><br>
> ```<br>
> {-# LANGUAGE DataKinds #-}<br>
><br>
> import Data.Proxy<br>
><br>
> data UserKind = User | Admin<br>
><br>
> data RealUser = RealUser { userAdminToken :: Maybe (Proxy 'Admin) }<br>
><br>
> doSensitiveThings :: Proxy 'Admin -> IO ()<br>
> doSensitiveThings = undefined<br>
> ```<br>
><br>
>> Also, I don't understand how I could define a type `Proxy 'Admin`. If<br>
>> I'm not wrong, `Proxy` should have the kind `UserType -> *`, but I<br>
>> don't know how to do that.<br>
><br>
> You can define it like:<br>
><br>
> data Proxy (a :: k) = Proxy<br>
><br>
> but that requires the {-# LANGUAGE PolyKinds #-} language extension<br>
><br>
>> Besides that, I would like some guidance in the general idea of the<br>
>> example, because I'm quite puzzled :)<br>
><br>
> The idea is that to restrict the type of the 'doSensitiveThings'<br>
> function so that you can only call it if you have "admin powers". To<br>
> prove that you have those admin powers you have to pass it a value of<br>
> type 'Proxy Admin'.<br>
><br>
> Let me maybe adapt the example slightly again to make things clearer:<br>
><br>
> ```<br>
> {-# LANGUAGE DataKinds #-}<br>
> {-# LANGUAGE PolyKinds #-}<br>
> data UserKind = User | Admin<br>
><br>
> data RealUser (uk :: UserKind) = RealUser { userName :: String }<br>
><br>
> root :: RealUser 'Admin<br>
> root = RealUser "root"<br>
><br>
> frank :: RealUser 'User<br>
> frank = RealUser "frank"<br>
><br>
> doSensitiveThings :: RealUser 'Admin -> IO ()<br>
> doSensitiveThings _ = print "installing packages now ... "<br>
><br>
> -- | this compiles fine:<br>
> testAllowed = doSensitiveThings root<br>
><br>
><br>
> -- | This gives a type error:<br>
> testNotAllowed = doSensitiveThings frank<br>
> -- • Couldn't match type ‘'User’ with ‘'Admin’<br>
> -- Expected type: RealUser 'Admin<br>
> -- Actual type: RealUser 'User<br>
> -- • In the first argument of ‘doSensitiveThings’, namely ‘frank’<br>
> -- In the expression: doSensitiveThings frank<br>
> -- In an equation for ‘testNotAllowed’:<br>
> -- testNotAllowed = doSensitiveThings frank<br>
> ```<br>
><br>
> In the above example, I've "tagged" the RealUser type with a type<br>
> variable that expresses if our user is a regular user or an Admin, and<br>
> our 'doSensitiveThings' function can only be called with Users that are<br>
> admins.<br>
><br>
> I hope this helps<br>
><br>
> --<br>
><br>
> - Frank<br>
>_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr">Javran (Fang) Cheng<br></div></div>