[Haskell-cafe] Help with DataKinds example

Marc Busqué marc at lamarciana.com
Sat Nov 24 07:59:17 UTC 2018


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
>


More information about the Haskell-Cafe mailing list