Record syntax, reopening a can of worms.

Hello list, As my first post. I'd like to open a can of worms that I sure has been opened before. That is record syntax. As we all know, there are some type safety problems with our current record syntax. The most obvious is that this compiles without even giving you a warning:
data MyData = A {a::Int, b::Int} | B {c::Int}
foo :: MyData -> Int foo a@A{} = c a
main :: IO () main = print $ foo (A 1 2)
This compiles, then crashes at run time. Rediculus, why didn't the glorious GHC catch this? This is not some ambigious scenario... One way I found to improve type checking is this:
data MyData = A A' | B B'
data A' = A'{a::Int, b::Int} data B' = B'{c::Int}
foo :: MyData -> Int foo (A a) = c a
main :: IO () main = print $ foo (A (A' 1 2))
This doesn't compile anymore because a :: A' and c :: B' -> X It seems like the later method is simply better. Better type checking = fewer runtime errors(I actually ran into a crash in a real project because of this lack of proper type checking...). Can we have a nice sugar for doing the later method? Thank you for your time, Timothy

Is it any more ridiculous than
f x@Nothing {} = fromJust x main = print (f Nothing)
crashing at run time? That is what you are expressing with your first one. This issue is completely unrelated to the named field syntax, they behave exactly like data types with non-named fields. However, you can achieve something like what you want with phantom types.
data ALike data BLike
data MyData t = A {a::Int, b::Int} | B {c::Int}
mkA x y = A x y :: MyData ALike mkB x = B x :: MyData BLike
then you can write functions of 'MyData ALike' to indicate it will only have 'A' as a constructor 'MyData BLike' to indicate it will only have 'B' and 'forall t . MyData t' for functions that can take a general MyData that can have either. John

Your Maybe example is very contrived. The place where I ran into this was much less contrived I think. I have an editor for a visual programming language. That looks like this: https://github.com/timthelion/gridhaskell-haskarrow/wiki I'm using a modified version of the Document-View model for application design. The commands in the language are defined in the Cell data type: https://github.com/timthelion/gridhaskell-haskarrow/blob/master/Cell.lhs Some Cell types, like Jump, have a long crooked line comming out of them called a Path. This line is held in the path :: Maybe Path feild. When I'm drawing the Cell tree, I have a function that extracts these Paths. https://github.com/timthelion/gridhaskell-haskarrow/blob/master/ ArrowDrawing.lhs#L75 It used to be, that more types of Cell than just the Jump Cell had a path. As I removed these Paths from the Cell datatype, my line drawing function started crashing, whenever it encountered those Cell types. By having chosen to use the short hand record selector syntax rather than the long hand place value syntax, I caused a runtime error in my code. I could of course have written the same function like this: <div id='LC69' class='line' style='background-color: transparent;'><span class='cs'>> </span><span class='kr'>where</span> <span class='n'>path_points</span> <span class='ow'>=</span> </div><div id='LC70' class='line' style='background-color: transparent;'><span class='cs'>> </span><span class='kr'>case</span></div><div id='LC71' class='line' style='background-color: transparent;'><span class='cs'>> </span><span class='kr'>case</span> <span class='n'>cell</span> <span class='kr'>of</span></div><div id='LC72' class='line' style='background-color: transparent;'><br></div><div id='LC73' class='line' style='background-color: transparent;'>Types of cells which have paths:</div><div id='LC74' class='line' style='background-color: transparent;'><br></div><div id='LC75' class='line' style='background-color: rgb(255, 255, 204);'><span class='cs'>> </span><span class='kt'>Cell</span><span class='o'>.</span><span class='kt'>Jump</span><span class='p'> _ path</span> <span class='ow'>-></span> Just path<span class='kt'></span></div><div id='LC76' class='line' style='background-color: transparent;'><span class='cs'>> </span><span class='kr'>_</span> <span class='ow'>-></span> <span class='kt'>Nothing of</span></div><div id='LC77' class='line' style='background-color: transparent;'><span class='cs'>> </span><span class='kr'>Just path -></span> <span class='n'>maybe</span> <span class='kt'>[]</span> <span class='p'>(</span><span class='nf'>\</span><span class='n'>p</span> <span class='ow'>-></span> <span class='p'>[</span><span class='kt'>Path</span><span class='o'>.</span><span class='n'>point</span> <span class='n'>p</span><span class='p'>])</span> <span class='p'>(</span><span class='kt'>Cell</span><span class='o'>.</span><span class='n'>path</span> <span class='n'>cell</span><span class='p'>)</span></div><div id='LC78' class='line' style='background-color: transparent;'><span class='cs'>> </span><span class='kr'>Nothing -></span> <span class='kt'>[]</span></div> Record selection is a more convenient syntax. It *could* be usefull for making more maintainable code(the reason why I choose it). The method I have chosen *would* be more maintainable in the case I want to add another feild to Jump. In that case I would not have to re-write the path_points function. Sadly, due to GHC's unnessesary and complete inability to do type safety checking, what should have been a convenient tool, has become an unnessecary source of runtime errors! How would I use your syntax in functions that want to pattern match against both A and B? I tried this without success:
data ALike data BLike
data MyData t = A {a::Int, b::Int} | B {c::Int}
mkA x y = A x y :: MyData ALike mkB x = B x :: MyData BLike
altRecordSyntaxes.lhs:15:18: Couldn't match type `BLike' with `ALike' Expected type: MyData ALike Actual type: MyData t In the first argument of `g', namely `myA' In the expression: g myA
foo :: MyData t -> Int
foo myA@A{} = g myA
where
g :: MyData ALike -> Int
g myA' = a myA'
foo myB@B{} = g myB
where
g :: MyData BLike -> Int
g myB' = c myB'
main :: IO ()
main = do
print $ foo $ mkA 1 3
This also doesn't work:
foo :: MyData t -> Int
foo myData =
case myData of
myA@A{} -> fooForA's myA
myB@B{} -> fooForB's myB
where
fooForA's :: MyData ALike -> Int
fooForA's myA' = a myA'
fooForB's :: MyData BLike -> Int
fooForB's myB' = a myB'
main :: IO ()
main = do
print $ foo $ mkA 1 3
My solution looks very clean(except for that nasty looking data declaration) and has the same advantages. Really, the current record syntax is just flawed :D
data MyData = A A' | B B'
data A' = A'{a::Int, b::Int} data B' = B'{c::Int}
foo :: MyData -> Int foo (A myA) = a myA foo (B myB) = c myB
main :: IO () main = print $ foo (A (A' 1 2))
Timothy
---------- Původní zpráva ----------
Od: John Meacham
f x@Nothing {} = fromJust x main = print (f Nothing)
crashing at run time? That is what you are expressing with your first one. This issue is completely unrelated to the named field syntax, they behave exactly like data types with non-named fields. However, you can achieve something like what you want with phantom types.
data ALike data BLike
data MyData t = A {a::Int, b::Int} | B {c::Int}
mkA x y = A x y :: MyData ALike mkB x = B x :: MyData BLike
then you can write functions of 'MyData ALike' to indicate it will only have 'A' as a constructor 'MyData BLike' to indicate it will only have 'B' and 'forall t . MyData t' for functions that can take a general MyData that can have either. John"

case myData of myA@A{} -> fooForA's myA myB@B{} -> fooForB's myB
I think this would typecheck if you used GADTs.
Actually what you'd want is to use the record syntax with GADTs (there are
to add the extra type safety you want), however both are not compatible.
data ALike
data BLike
data MyData x where
A :: Int -> Int -> MyData ALike
B :: Int -> MyData BLike
a (A x _) = x
b (A _ x) = x
c (B x) = x
-- GHC may require you to write the type signatures for those three
functions.
Le 27 mai 2012 10:52,
Your Maybe example is very contrived. The place where I ran into this was much less contrived I think.
I have an editor for a visual programming language. That looks like this:
https://github.com/timthelion/gridhaskell-haskarrow/wiki
I'm using a modified version of the Document-View model for application design. The commands in the language are defined in the Cell data type:
https://github.com/timthelion/gridhaskell-haskarrow/blob/master/Cell.lhs
Some Cell types, like Jump, have a long crooked line comming out of them called a Path. This line is held in the path :: Maybe Path feild.
When I'm drawing the Cell tree, I have a function that extracts these Paths. https://github.com/timthelion/gridhaskell-haskarrow/blob/master/ArrowDrawing...
It used to be, that more types of Cell than just the Jump Cell had a path.
As I removed these Paths from the Cell datatype, my line drawing function started crashing, whenever it encountered those Cell types. By having chosen to use the short hand record selector syntax rather than the long hand place value syntax, I caused a runtime error in my code.
I could of course have written the same function like this:
where path_points = case case cell of
Types of cells which have paths:
Cell.Jump _ path -> Just path _ -> Nothing of Just path -> maybe [] (\p -> [Path.point p]) (Cell.path cell) Nothing -> []
Record selection is a more convenient syntax. It *could* be usefull for making more maintainable code(the reason why I choose it). The method I have chosen *would* be more maintainable in the case I want to add another feild to Jump. In that case I would not have to re-write the path_points function. Sadly, due to GHC's unnessesary and complete inability to do type safety checking, what should have been a convenient tool, has become an unnessecary source of runtime errors!
How would I use your syntax in functions that want to pattern match against both A and B? I tried this without success:
data ALike data BLike
data MyData t = A {a::Int, b::Int} | B {c::Int}
mkA x y = A x y :: MyData ALike mkB x = B x :: MyData BLike
altRecordSyntaxes.lhs:15:18: Couldn't match type `BLike' with `ALike' Expected type: MyData ALike Actual type: MyData t In the first argument of `g', namely `myA' In the expression: g myA
foo :: MyData t -> Int
foo myA@A{} = g myA
where
g :: MyData ALike -> Int
g myA' = a myA'
foo myB@B{} = g myB
where
g :: MyData BLike -> Int
g myB' = c myB'
main :: IO ()
main = do
print $ foo $ mkA 1 3
This also doesn't work:
foo :: MyData t -> Int
foo myData =
case myData of
myA@A{} -> fooForA's myA
myB@B{} -> fooForB's myB
where
fooForA's :: MyData ALike -> Int
fooForA's myA' = a myA'
fooForB's :: MyData BLike -> Int
fooForB's myB' = a myB'
main :: IO ()
main = do
print $ foo $ mkA 1 3
My solution looks very clean(except for that nasty looking data declaration) and has the same advantages. Really, the current record syntax is just flawed :D
data MyData = A A' | B B'
data A' = A'{a::Int, b::Int} data B' = B'{c::Int}
foo :: MyData -> Int foo (A myA) = a myA foo (B myB) = c myB
main :: IO () main = print $ foo (A (A' 1 2))
Timothy
---------- Původní zpráva ---------- Od: John Meacham
Datum: 27. 5. 2012 Předmět: Re: [Haskell-cafe] Record syntax, reopening a can of worms. Is it any more ridiculous than
f x@Nothing {} = fromJust x main = print (f Nothing)
crashing at run time? That is what you are expressing with your first one. This issue is completely unrelated to the named field syntax, they behave exactly like data types with non-named fields.
However, you can achieve something like what you want with phantom types.
data ALike data BLike
data MyData t = A {a::Int, b::Int} | B {c::Int}
mkA x y = A x y :: MyData ALike mkB x = B x :: MyData BLike
then you can write functions of 'MyData ALike' to indicate it will only have 'A' as a constructor 'MyData BLike' to indicate it will only have 'B' and 'forall t . MyData t' for functions that can take a general MyData that can have either.
John
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Somehow I don't understand you.
Could you please fill out your example into a working bit of code?
Thank you,
Timothy
---------- Původní zpráva ----------
Od: Yves Parès
case myData of myA@A{} -> fooForA's myA myB@B{} -> fooForB's myB
I think this would typecheck if you used GADTs.
Actually what you'd want is to use the record syntax with GADTs (there are
to add the extra type safety you want), however both are not compatible.
data ALike
data BLike
data MyData x where
A :: Int -> Int -> MyData ALike
B :: Int -> MyData BLike
a (A x _) = x
b (A _ x) = x
c (B x) = x
-- GHC may require you to write the type signatures for those three
functions.
Le 27 mai 2012 10:52, a écrit :
"
Your Maybe example is very contrived. The place where I ran into this was
much less contrived I think. I have an editor for a visual programming language. That looks like this:
https://github.com/timthelion/gridhaskell-haskarrow/wiki
(https://github.com/timthelion/gridhaskell-haskarrow/wiki)
I'm using a modified version of the Document-View model for application
design. The commands in the language are defined in the Cell data type:
https://github.com/timthelion/gridhaskell-haskarrow/blob/master/Cell.lhs
(https://github.com/timthelion/gridhaskell-haskarrow/blob/master/Cell.lhs)
Some Cell types, like Jump, have a long crooked line comming out of them
called a Path. This line is held in the path :: Maybe Path feild.
When I'm drawing the Cell tree, I have a function that extracts these Paths.
https://github.com/timthelion/gridhaskell-haskarrow/blob/master/
ArrowDrawing.lhs#L75
(https://github.com/timthelion/gridhaskell-haskarrow/blob/master/ArrowDrawing...)
It used to be, that more types of Cell than just the Jump Cell had a path.
As I removed these Paths from the Cell datatype, my line drawing function
started crashing, whenever it encountered those Cell types. By having
chosen to use the short hand record selector syntax rather than the long
hand place value syntax, I caused a runtime error in my code.
I could of course have written the same function like this:
<div style='background-color:transparent'><span>> </span><span>where</span> <span>path_points</span> <span>=</span> </div><div style='background-color:transparent'>
<span>> </span><span>case</span></div><div style='background-color:transparent'><span>> </span><span>case</span> <span>cell</span> <span>of</span></div><div style='background-color:transparent'><br>
</div><div style='background-color:transparent'>Types of cells which have paths:</div><div style='background-color:transparent'><br></div><div style='background-color:rgb(255,255,204)'><span>> </span><span>Cell</span><span>.</span><span>Jump</span><span> _ path</span> <span>-></span> Just path<span></span></div>
<div style='background-color:transparent'><span>> </span><span>_</span> <span>-></span> <span>Nothing of</span></div><div style='background-color:transparent'><span>> </span><span>Just path -></span> <span>maybe</span> <span>[]</span> <span>(</span><span>\</span><span>p</span> <span>-></span> <span>[</span><span>Path</span><span>.</span><span>point</span> <span>p</span><span>])</span> <span>(</span><span>Cell</span><span>.</span><span>path</span> <span>cell</span><span>)</span></div>
<div style='background-color:transparent'><span>> </span><span>Nothing -></span> <span>[]</span></div>
Record selection is a more convenient syntax. It *could* be usefull for
making more maintainable code(the reason why I choose it). The method I
have chosen *would* be more maintainable in the case I want to add another
feild to Jump. In that case I would not have to re-write the path_points
function. Sadly, due to GHC's unnessesary and complete inability to do type
safety checking, what should have been a convenient tool, has become an
unnessecary source of runtime errors!
How would I use your syntax in functions that want to pattern match against
both A and B? I tried this without success: data ALike
data BLike data MyData t = A {a::Int,
b::Int} |
B {c::Int} mkA x y = A x y :: MyData ALike
mkB x = B x :: MyData BLike altRecordSyntaxes.lhs:15:18:
Couldn't match type `BLike' with `ALike'
Expected type: MyData ALike
Actual type: MyData t
In the first argument of `g', namely `myA'
In the expression: g myA foo :: MyData t -> Int foo myA@A{} = g myA where g :: MyData ALike -> Int g myA' = a myA' foo myB@B{} = g myB where g :: MyData BLike -> Int g myB' = c myB' main :: IO () main = do print $ foo $ mkA 1 3 This also doesn't work: foo :: MyData t -> Int foo myData = case myData of myA@A{} -> fooForA's myA myB@B{} -> fooForB's myB where fooForA's :: MyData ALike -> Int fooForA's myA' = a myA' fooForB's :: MyData BLike -> Int fooForB's myB' = a myB' main :: IO () main = do print $ foo $ mkA 1 3 My solution looks very clean(except for that nasty looking data declaration)
and has the same advantages. Really, the current record syntax is just
flawed :D data MyData = A A' | B B' data A' = A'{a::Int,
b::Int}
data B' = B'{c::Int} foo :: MyData -> Int
foo (A myA) = a myA
foo (B myB) = c myB main :: IO ()
main = print $ foo (A (A' 1 2)) Timothy
---------- Původní zpráva ----------
Od: John Meacham f x@Nothing {} = fromJust x
main = print (f Nothing) crashing at run time? That is what you are expressing with your first
one. This issue is completely unrelated to the named field syntax,
they behave exactly like data types with non-named fields.
However, you can achieve something like what you want with phantom types. data ALike
data BLike data MyData t = A {a::Int,
b::Int} |
B {c::Int} mkA x y = A x y :: MyData ALike
mkB x = B x :: MyData BLike then you can write functions of
'MyData ALike' to indicate it will only have 'A' as a constructor
'MyData BLike' to indicate it will only have 'B'
and 'forall t . MyData t' for functions that can take a general MyData
that can have either.
John"
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org(mailto:Haskell-Cafe@haskell.org)
http://www.haskell.org/mailman/listinfo/haskell-cafe
(http://www.haskell.org/mailman/listinfo/haskell-cafe)
"
"

I enclosed a source file that shows the use of a GADT in that case.
2012/5/27
Somehow I don't understand you. Could you please fill out your example into a working bit of code?
Thank you,
Timothy
---------- Původní zpráva ---------- Od: Yves Parès
Datum: 27. 5. 2012 Předmět: Re: [Haskell-cafe] Record syntax, reopening a can of worms.
case myData of myA@A{} -> fooForA's myA myB@B{} -> fooForB's myB
I think this would typecheck if you used GADTs. Actually what you'd want is to use the record syntax with GADTs (there are to add the extra type safety you want), however both are not compatible.
data ALike data BLike
data MyData x where A :: Int -> Int -> MyData ALike B :: Int -> MyData BLike
a (A x _) = x b (A _ x) = x c (B x) = x -- GHC may require you to write the type signatures for those three functions. Le 27 mai 2012 10:52,
a écrit : Your Maybe example is very contrived. The place where I ran into this was much less contrived I think.
I have an editor for a visual programming language. That looks like this:
https://github.com/timthelion/gridhaskell-haskarrow/wiki
I'm using a modified version of the Document-View model for application design. The commands in the language are defined in the Cell data type:
https://github.com/timthelion/gridhaskell-haskarrow/blob/master/Cell.lhs
Some Cell types, like Jump, have a long crooked line comming out of them called a Path. This line is held in the path :: Maybe Path feild.
When I'm drawing the Cell tree, I have a function that extracts these Paths. https://github.com/timthelion/gridhaskell-haskarrow/blob/master/ArrowDrawing...
It used to be, that more types of Cell than just the Jump Cell had a path.
As I removed these Paths from the Cell datatype, my line drawing function started crashing, whenever it encountered those Cell types. By having chosen to use the short hand record selector syntax rather than the long hand place value syntax, I caused a runtime error in my code.
I could of course have written the same function like this:
where path_points =
case case cell of
Types of cells which have paths:
Cell.Jump _ path -> Just path
_ -> Nothing of Just path -> maybe [] (\p -> [Path.point p]) (Cell.path cell)
Nothing -> []
Record selection is a more convenient syntax. It *could* be usefull for making more maintainable code(the reason why I choose it). The method I have chosen *would* be more maintainable in the case I want to add another feild to Jump. In that case I would not have to re-write the path_points function. Sadly, due to GHC's unnessesary and complete inability to do type safety checking, what should have been a convenient tool, has become an unnessecary source of runtime errors!
How would I use your syntax in functions that want to pattern match against both A and B? I tried this without success:
data ALike data BLike
data MyData t = A {a::Int, b::Int} | B {c::Int}
mkA x y = A x y :: MyData ALike mkB x = B x :: MyData BLike
altRecordSyntaxes.lhs:15:18: Couldn't match type `BLike' with `ALike' Expected type: MyData ALike Actual type: MyData t In the first argument of `g', namely `myA' In the expression: g myA
foo :: MyData t -> Int
foo myA@A{} = g myA
where
g :: MyData ALike -> Int
g myA' = a myA'
foo myB@B{} = g myB
where
g :: MyData BLike -> Int
g myB' = c myB'
main :: IO ()
main = do
print $ foo $ mkA 1 3
This also doesn't work:
foo :: MyData t -> Int
foo myData =
case myData of
myA@A{} -> fooForA's myA
myB@B{} -> fooForB's myB
where
fooForA's :: MyData ALike -> Int
fooForA's myA' = a myA'
fooForB's :: MyData BLike -> Int
fooForB's myB' = a myB'
main :: IO ()
main = do
print $ foo $ mkA 1 3
My solution looks very clean(except for that nasty looking data declaration) and has the same advantages. Really, the current record syntax is just flawed :D
data MyData = A A' | B B'
data A' = A'{a::Int, b::Int} data B' = B'{c::Int}
foo :: MyData -> Int foo (A myA) = a myA foo (B myB) = c myB
main :: IO () main = print $ foo (A (A' 1 2))
Timothy
---------- Původní zpráva ---------- Od: John Meacham
Datum: 27. 5. 2012 Předmět: Re: [Haskell-cafe] Record syntax, reopening a can of worms. Is it any more ridiculous than
f x@Nothing {} = fromJust x main = print (f Nothing)
crashing at run time? That is what you are expressing with your first one. This issue is completely unrelated to the named field syntax, they behave exactly like data types with non-named fields.
However, you can achieve something like what you want with phantom types.
data ALike data BLike
data MyData t = A {a::Int, b::Int} | B {c::Int}
mkA x y = A x y :: MyData ALike mkB x = B x :: MyData BLike
then you can write functions of 'MyData ALike' to indicate it will only have 'A' as a constructor 'MyData BLike' to indicate it will only have 'B' and 'forall t . MyData t' for functions that can take a general MyData that can have either.
John
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (3)
-
John Meacham
-
timothyhobbs@seznam.cz
-
Yves Parès