[Haskell-cafe] Help with DataKinds example

[Javran Cheng]

Hi Marc,

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.

Cheers,
Javran

On Fri, Nov 23, 2018 at 11:59 PM Marc Busqué <marc at lamarciana.com> wrote:

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



-- 
Javran (Fang) Cheng
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181124/14c2ad4c/attachment.html>