[Haskell-cafe] Help with DataKinds example

[Marc Busqué]

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?

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.

Besides that, I would like some guidance in the general idea of the
example, because I'm quite puzzled :)

Thanks in advance!

Marc Busqué
http://waiting-for-dev.github.io/about/

[Frank Staals]

Post by Marc Busqué
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.
```
data UserType = User | Admin
```
```
data User = User
{ userAdminToken :: Maybe (Proxy 'Admin) }
```
And then it is said that we can enforce that sensitive operations are
```
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
```

Post by Marc Busqué
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

Post by Marc Busqué
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

[Marc Busqué]

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/

Post by Frank Staals

Post by Marc Busqué
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.
```
data UserType = User | Admin
```
```
data User = User
{ userAdminToken :: Maybe (Proxy 'Admin) }
```
And then it is said that we can enforce that sensitive operations are
```
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
```
{-# LANGUAGE DataKinds #-}
import Data.Proxy
data UserKind = User | Admin
data RealUser = RealUser { userAdminToken :: Maybe (Proxy 'Admin) }
doSensitiveThings :: Proxy 'Admin -> IO ()
doSensitiveThings = undefined
```

Post by Marc Busqué
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.

data Proxy (a :: k) = Proxy
but that requires the {-# LANGUAGE PolyKinds #-} language extension

Post by Marc Busqué
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'.
```
{-# 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 ... "
testAllowed = doSensitiveThings root
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
-- 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

[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

Post by Marc Busqué
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
```
{-# 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/

Post by Frank Staals

Post by Marc Busqué
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.
```
data UserType = User | Admin
```
```
data User = User
{ userAdminToken :: Maybe (Proxy 'Admin) }
```
And then it is said that we can enforce that sensitive operations are
```
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'

Post by Frank Staals
constructor in the UserType type. It may be clearer if we slightly
```
{-# LANGUAGE DataKinds #-}
import Data.Proxy
data UserKind = User | Admin
data RealUser = RealUser { userAdminToken :: Maybe (Proxy 'Admin) }
doSensitiveThings :: Proxy 'Admin -> IO ()
doSensitiveThings = undefined
```

Post by Marc Busqué
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.

data Proxy (a :: k) = Proxy
but that requires the {-# LANGUAGE PolyKinds #-} language extension

Post by Marc Busqué
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'.
```
{-# 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 ... "
testAllowed = doSensitiveThings root
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
-- 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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.