phantom types and record syntax

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

phantom types and record syntax

Dimitri DeFigueiredo
Hi All,

My apologies if this is not the right forum, but am not satisfied with my current understanding.

I am surprised that this program compiles in GHC:

-----
data UserSupplied  = UserSupplied -- i.e. unsafe
data Safe          = Safe

data Username a = Username { first :: String, last :: String}

sanitize :: Username UserSupplied -> Username Safe
sanitize name = name { first = "John" }

main = putStrLn "Hi!"
-----

My trouble is that it seems the record syntax is *implicitly* converting from one type to the other. It seems I would have to remove the phantom type by adding a tag to avoid this:

-----
data Username a = Username { first :: String, last :: String, tag :: a }

sanitize :: Username UserSupplied -> Username Safe
sanitize name = name { first = "John" } -- FAIL as expected!! :-)
-----

But this makes me unwilling to use phantom types for security as I would be worried of unwittingly making the conversion.

Could somebody sprinkle some insight into why this is "converted automatically" for phantom types?
Is there another way around this?


Thanks!


Dimitri



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: phantom types and record syntax

Tikhon Jelvis
Record updates have to be able to change the type of the value in order to work with polymorphic fields. Here's a contrived example:

data Foo a = Foo { foo :: a }

reFoo x = x { foo = "blarg" }

By the same logic, the resulting type can change the phantom parameter because the phantom parameter is not constrained at all. You could have the same problem without record syntax:

unsafeId (Username first last) = Username first last

That looks fine—but completely bypasses the phantom type! (In fact, it could even produce a Username Int or something.)

This is a fundamental limitation of phantom types. Since they're not constrained at all, they're very easy to change. They're useful, but more as a convention and a warning than as an ironclad guarantee.

In this specific case, I can think of two reasonable options. One is to make the Username type abstract—don't export the constructor and ensure that the only provided ways to make one are safe. Another is to make a String newtype with a flag, and keep that abstract. Domain-specific types like Username could use this newtype for their fields.

newtype Str a = Str String

data Username a = Username { first :: Str a, last :: Str a }

As long as you have access to a Str constructor, you can make "Safe" instances however you like; however, if you keep the type abstract, it can be safe outside the defining module.

There are some other design options, and it's something worth thinking about. But what you've found is a fundamental quality (and limitation) of phantom types and has to be kept in mind as you're working with them.


On Wed, Jun 17, 2015 at 7:45 PM, Dimitri DeFigueiredo <[hidden email]> wrote:
Hi All,

My apologies if this is not the right forum, but am not satisfied with my current understanding.

I am surprised that this program compiles in GHC:

-----
data UserSupplied  = UserSupplied -- i.e. unsafe
data Safe          = Safe

data Username a = Username { first :: String, last :: String}

sanitize :: Username UserSupplied -> Username Safe
sanitize name = name { first = "John" }

main = putStrLn "Hi!"
-----

My trouble is that it seems the record syntax is *implicitly* converting from one type to the other. It seems I would have to remove the phantom type by adding a tag to avoid this:

-----
data Username a = Username { first :: String, last :: String, tag :: a }

sanitize :: Username UserSupplied -> Username Safe
sanitize name = name { first = "John" } -- FAIL as expected!! :-)
-----

But this makes me unwilling to use phantom types for security as I would be worried of unwittingly making the conversion.

Could somebody sprinkle some insight into why this is "converted automatically" for phantom types?
Is there another way around this?


Thanks!


Dimitri



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: phantom types and record syntax

Chaddaï Fouché
In reply to this post by Dimitri DeFigueiredo
Le jeu. 18 juin 2015 à 04:45, Dimitri DeFigueiredo <[hidden email]> a écrit :
I am surprised that this program compiles in GHC:

snip

My trouble is that it seems the record syntax is *implicitly* converting from one type to the other. It seems I would have to remove the phantom type by adding a tag to avoid this:

This is faulty reasoning because it imply that a value changed type in your code, based on your understanding that the record syntax is "changing" a value...

This is not the case ! Haskell is functional, immutability is the rule. The record syntax is just a shortcut to create a new value sharing some of its parts with the old value. It is thus perfectly normal that the type of this new value can be different of the type of the old value if no other constraint prevent this (and Phantom types are by essence unconstrained by the value, that is why they're "Phantom").
 

But this makes me unwilling to use phantom types for security as I would be worried of unwittingly making the conversion.


The value of Phantom types is generally only displayed if you make them abstract types, since the only way to constrain the phantom type is by imposing restrictive signatures for your handling functions (and then using those restricted functions)... This is why you usually won't export the constructors, only smart constructors that can only produce a precise type of value with the right phantom type. In these conditions, you can't "unwittingly make a conversion" and your API impose a safe pattern of use, helped by the type system to interdict unsafe combination without any runtime cost.
 

Could somebody sprinkle some insight into why this is "converted automatically" for phantom types?
Is there another way around this?


As I said, your perspective is wrong : there is no "conversion" here, simply a new value with a new type. I really fail to see why you would want your program to fail to compile, your "sanitize" is exactly the kind of function Phantom types are for : supposing you can only create "Username UserSupplied" with your API, and a part of your API only accept "Username Safe", you'll need a function like sanitize to bridge those two parts.

--
Jedaï

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe