phantom types and record syntax

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

phantom types and record syntax

Dimitri DeFigueiredo
Hi All,

I am a little suprised that this program compiles in GHC:

----
data ReqTime = ReqTime
data AckTime = AckTime

data Order a = Order { price  ::Double, volume ::Int, timestamp ::Int }

convertToReq :: Order AckTime -> Order ReqTime
convertToReq o = o{price = 1}

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 to avoid this:

----
data Order a = Order { price  ::Double, volume ::Int, timestamp ::Int,
myType :: a }

convertToReq :: Order AckTime -> Order ReqTime
convertToReq o = o{price = 1}  -- fail!!
----

Could somebody sprinkle some insight into why this is "converted
automatically" for phantom types? Can I avoid this behavior?

Thanks!

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

Re: phantom types and record syntax

akash g
The phantom type doesn't appear on the actual constructors, only on the  type signatures.  In the function convertToReq, you are changing the following
1. The type.
2. The value of the price record (actually returning a new value with the price record changed to one and the rest of the fields being the same.



That said, I don't see the point of a phantom on a record structure like this.  Phantoms are more useful when you have multiple data constructors for a given type and you want to make sure you don't have constructions that don't make sense.  Like in an interpreter, you don't want to create expressions that can give rise to an expressions like add a integer to a string and that sort of thing.


In fact, that set of lecture notes as well as the 2014 class notes are amazingly good.


On Wed, Jun 17, 2015 at 6:13 AM, Dimitri DeFigueiredo <[hidden email]> wrote:
Hi All,

I am a little suprised that this program compiles in GHC:

----
data ReqTime = ReqTime
data AckTime = AckTime

data Order a = Order { price  ::Double, volume ::Int, timestamp ::Int }

convertToReq :: Order AckTime -> Order ReqTime
convertToReq o = o{price = 1}

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 to avoid this:

----
data Order a = Order { price  ::Double, volume ::Int, timestamp ::Int, myType :: a }

convertToReq :: Order AckTime -> Order ReqTime
convertToReq o = o{price = 1}  -- fail!!
----

Could somebody sprinkle some insight into why this is "converted automatically" for phantom types? Can I avoid this behavior?

Thanks!

Dimitri
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


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

Re: phantom types and record syntax

Brandon Allbery
On Wed, Jun 17, 2015 at 12:14 AM, akash g <[hidden email]> wrote:
The phantom type doesn't appear on the actual constructors, only on the  type signatures.  In the function convertToReq, you are changing the following
1. The type.
2. The value of the price record (actually returning a new value with the price record changed to one and the rest of the fields being the same.

I'm not sure I see the difference between the given example and the "effectively phantom" type in

    foo :: Maybe String -> Maybe Int
    foo x@Nothing = x -- error: Nothing :: Maybe String is not compatible with Maybe Int
    foo x = ...

--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

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

Re: phantom types and record syntax

akash g
When you have phantom types, you get can catch logically illegal functions in the type itself.  You can create constructors for types so that you can't create illegal expressions.
-----------------
data Expr = Num Int             -- atom
          | Str String          -- atom
          | Op BinOp Expr Expr  -- compound
            deriving (Show)

data BinOp = Add | Concat
             deriving (Show)

data Expr1 a = Num1 Int             -- atom
            | Str1 String          -- atom
            | Op1 BinOp (Expr1 a) (Expr1 a)  -- compound
            deriving (Show)

addition :: Expr1 Int -> Expr1 Int -> Expr1 Int
addition (Num1 a) (Num1 b) = Num1 $ a + b

createNum :: Int -> Expr
createNum a = Num a

createStr :: String -> Expr
createStr a = Str a

createNum1 :: Int -> Expr1 Int
createNum1 a = Num1 a


createStr1 :: String -> Expr1 String
createStr1 a = Str1 a


sumExpr :: Expr -> Expr -> Expr
sumExpr a b = Op Add a b

sumExpr1 :: Expr1 Int -> Expr1 Int -> Expr1 Int
sumExpr1 a b = Op1 Add a b

-----------------

With the above, you can create expressions that make no sense in real life (like adding/concating a number to a string ).  When I execute this in GHCI, I get the following

--------
λ> sumExpr (createNum 1) (createStr "a")
Op Add (Num 1) (Str "a")
λ> sumExpr1 (createNum1 1) (createStr1 "a")

<interactive>:342:26-39:
    Couldn't match type ‘[Char]’ with ‘Int’
    Expected type: Expr1 Int
      Actual type: Expr1 String
    In the second argument of ‘sumExpr1’, namely ‘(createStr1 "a")’
    In the expression: sumExpr1 (createNum1 1) (createStr1 "a")
λ>
--------

From the above, it is clear that as long as we write constructors taking into account the types (called smart-constructors), we can prevent expressions from being created.  I do admit that this makes it a bit tedious as we would have to write the constructors by hand, but we get type level guarantees.

I think GADTs are much better for things like this for specifying the constructors, but you'd still have to write sumExpr1 in program.


On Wed, Jun 17, 2015 at 10:25 AM, Brandon Allbery <[hidden email]> wrote:
On Wed, Jun 17, 2015 at 12:14 AM, akash g <[hidden email]> wrote:
The phantom type doesn't appear on the actual constructors, only on the  type signatures.  In the function convertToReq, you are changing the following
1. The type.
2. The value of the price record (actually returning a new value with the price record changed to one and the rest of the fields being the same.

I'm not sure I see the difference between the given example and the "effectively phantom" type in

    foo :: Maybe String -> Maybe Int
    foo x@Nothing = x -- error: Nothing :: Maybe String is not compatible with Maybe Int
    foo x = ...

--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners



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

Re: phantom types and record syntax

akash g
Oh, and the above data types were lifted from Stanford's cs240h (the 2011 version).

On Wed, Jun 17, 2015 at 11:04 AM, akash g <[hidden email]> wrote:
When you have phantom types, you get can catch logically illegal functions in the type itself.  You can create constructors for types so that you can't create illegal expressions.
-----------------
data Expr = Num Int             -- atom
          | Str String          -- atom
          | Op BinOp Expr Expr  -- compound
            deriving (Show)

data BinOp = Add | Concat
             deriving (Show)

data Expr1 a = Num1 Int             -- atom
            | Str1 String          -- atom
            | Op1 BinOp (Expr1 a) (Expr1 a)  -- compound
            deriving (Show)

addition :: Expr1 Int -> Expr1 Int -> Expr1 Int
addition (Num1 a) (Num1 b) = Num1 $ a + b

createNum :: Int -> Expr
createNum a = Num a

createStr :: String -> Expr
createStr a = Str a

createNum1 :: Int -> Expr1 Int
createNum1 a = Num1 a


createStr1 :: String -> Expr1 String
createStr1 a = Str1 a


sumExpr :: Expr -> Expr -> Expr
sumExpr a b = Op Add a b

sumExpr1 :: Expr1 Int -> Expr1 Int -> Expr1 Int
sumExpr1 a b = Op1 Add a b

-----------------

With the above, you can create expressions that make no sense in real life (like adding/concating a number to a string ).  When I execute this in GHCI, I get the following

--------
λ> sumExpr (createNum 1) (createStr "a")
Op Add (Num 1) (Str "a")
λ> sumExpr1 (createNum1 1) (createStr1 "a")

<interactive>:342:26-39:
    Couldn't match type ‘[Char]’ with ‘Int’
    Expected type: Expr1 Int
      Actual type: Expr1 String
    In the second argument of ‘sumExpr1’, namely ‘(createStr1 "a")’
    In the expression: sumExpr1 (createNum1 1) (createStr1 "a")
λ>
--------

From the above, it is clear that as long as we write constructors taking into account the types (called smart-constructors), we can prevent expressions from being created.  I do admit that this makes it a bit tedious as we would have to write the constructors by hand, but we get type level guarantees.

I think GADTs are much better for things like this for specifying the constructors, but you'd still have to write sumExpr1 in program.


On Wed, Jun 17, 2015 at 10:25 AM, Brandon Allbery <[hidden email]> wrote:
On Wed, Jun 17, 2015 at 12:14 AM, akash g <[hidden email]> wrote:
The phantom type doesn't appear on the actual constructors, only on the  type signatures.  In the function convertToReq, you are changing the following
1. The type.
2. The value of the price record (actually returning a new value with the price record changed to one and the rest of the fields being the same.

I'm not sure I see the difference between the given example and the "effectively phantom" type in

    foo :: Maybe String -> Maybe Int
    foo x@Nothing = x -- error: Nothing :: Maybe String is not compatible with Maybe Int
    foo x = ...

--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners




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

Re: phantom types and record syntax

Karl Voelker-2
In reply to this post by Dimitri DeFigueiredo
On Tue, Jun 16, 2015, at 05:43 PM, Dimitri DeFigueiredo wrote:

> I am a little suprised that this program compiles in GHC:
>
> ----
> data ReqTime = ReqTime
> data AckTime = AckTime
>
> data Order a = Order { price  ::Double, volume ::Int, timestamp ::Int }
>
> convertToReq :: Order AckTime -> Order ReqTime
> convertToReq o = o{price = 1}
>
> main = putStrLn "Hi!"
> ----

I found it surprising, too. But, if you look in the Haskell report
(https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-540003.15.3),
record update is defined by a "desugaring" translation. So your
convertToReq desugars (roughly) to:

convertToReq o = case o of
    Order v1 v2 v3 -> Order 1 v2 v3

Unfortunately, the report does not have any commentary on why it is the
way it is.

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

Re: phantom types and record syntax

Dimitri DeFigueiredo
Thanks for the thoughts.

This is funny, so the constructor has the same name but is for different
types. I think this is specially bad for security. I'm going to be
paranoid about it now.

Dimitri


On 17/06/15 00:42, Karl Voelker wrote:

> On Tue, Jun 16, 2015, at 05:43 PM, Dimitri DeFigueiredo wrote:
>> I am a little suprised that this program compiles in GHC:
>>
>> ----
>> data ReqTime = ReqTime
>> data AckTime = AckTime
>>
>> data Order a = Order { price  ::Double, volume ::Int, timestamp ::Int }
>>
>> convertToReq :: Order AckTime -> Order ReqTime
>> convertToReq o = o{price = 1}
>>
>> main = putStrLn "Hi!"
>> ----
> I found it surprising, too. But, if you look in the Haskell report
> (https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-540003.15.3),
> record update is defined by a "desugaring" translation. So your
> convertToReq desugars (roughly) to:
>
> convertToReq o = case o of
>      Order v1 v2 v3 -> Order 1 v2 v3
>
> Unfortunately, the report does not have any commentary on why it is the
> way it is.
>
> -Karl
> _______________________________________________
> Beginners mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

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

Re: phantom types and record syntax

Karl Voelker-2
On Wed, Jun 17, 2015, at 07:21 PM, Dimitri DeFigueiredo wrote:
> This is funny, so the constructor has the same name but is for different
> types. I think this is specially bad for security. I'm going to be
> paranoid about it now.

If you would like to give some more background on your use case, we may
be able to suggest better ways to ensure safety through types.

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

Re: phantom types and record syntax

Imants Cekusins
function signature makes a difference. in this example, try swapping
the signature of function convertToReq

it seems implicit conversion happens depending on signature (and usual
constraints), yes


module Phantom where

data ReqTime = ReqTime
data AckTime = AckTime


-- convertToReq :: Order AckTime -> Order ReqTime  -- builds
convertToReq :: Order AckTime -> Order AckTime  -- error
convertToReq o = o{price = 1}



data Order a = Order { price  ::Double, volume ::Int, timestamp ::Int }

main :: Order ReqTime
main =   expectReq conv
      where ack = initAckTime
            conv = convertToReq ack

initAckTime:: Order AckTime
initAckTime = Order {
   timestamp = 0,
   price = 2.1,
   volume = 3
   }



expectReq::Order ReqTime -> Order ReqTime
expectReq o = o
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners