| Then we can define
|
| safeCoerce :: (a ~~ b) = a - b
| safeCoerce = unsafeCoerce
Yes, that's right. When I said we have the technology I meant that we
(will) have something similar to ~~. See our paper Generative Type
Abstraction and Type-level Computation
| The exact syntax is a problem (as usual). We have the technology now. The
| question is how important it is.
|
| I think extending the syntax for contexts would be sufficient:
| Write a ~~ b for a can be converted to b by wrapping / unwrapping
| newtypes, which is a conservative
Simon Peyton-Jones wrote:
What you really want is to say is something like this. Suppose my_tree ::
Tree String. Then you'd like to say
my_tree ::: Tree Foo
meaning please find a way to convert m_tree to type (Tree Foo), using
newtype coercions.
The exact syntax is a problem
| Yes, you can freely use Foo/unFoo. There's no runtime penalty. (In the
| jargon of GHC's intermediate language, Foo and unFoo translate to
| *type-safe casts*, which generate no executable code.
|
| When does the conversion to type-safe casts occur relative to other
| optimizations
| At the end of the day what motivated me to ask these questions it that
| I like very much defining newtypes for most of the types I use, I have
| completely forgotten about `type' aliasing. I'm completely happy to
| write Foo and unFoo all over the place to aid my type correctness, but
| I
On 20 October 2010 13:09, Simon Peyton-Jones simo...@microsoft.com wrote:
Yes, you can freely use Foo/unFoo. There's no runtime penalty. (In the
jargon of GHC's intermediate language, Foo and unFoo translate to *type-safe
casts*, which generate no executable code.
That includes the
On Oct 20, 2010, at 11:58 AM, Gregory Crosswhite gcr...@phys.washington.edu
wrote:
On 10/20/10 4:09 AM, Simon Peyton-Jones wrote:
No, this isn't optimised. The trouble is that you write (map Foo xs), but
GHC doesn't know about 'map'. We could add a special case for map, but then
you'd
Do we really want to treat every newtype wrappers as a form of 'id'?
For example:
newtype Nat = Nat Integer -- must always be positive
A possible rule (doesn't actually typecheck, but you get the idea):
forall (x :: Nat). sqrt (x * x) = x
If we ignore newtyping we get an incorrect
On 10/20/10 7:09 AM, Simon Peyton-Jones wrote:
Yes, you can freely use Foo/unFoo. There's no runtime penalty. (In the jargon
of GHC's intermediate language, Foo and unFoo translate to *type-safe casts*,
which generate no executable code.
When does the conversion to type-safe casts occur
On Thursday 21 October 2010 01:11:25, wren ng thornton wrote:
On 10/20/10 7:07 PM, wren ng thornton wrote:
On 10/20/10 7:09 AM, Simon Peyton-Jones wrote:
Yes, you can freely use Foo/unFoo. There's no runtime penalty. (In
the jargon of GHC's intermediate language, Foo and unFoo translate to
On Oct 20, 2010, at 5:06 PM, Thomas Schilling nomin...@googlemail.com wrote:
Do we really want to treat every newtype wrappers as a form of 'id'?
For example:
newtype Nat = Nat Integer -- must always be positive
A possible rule (doesn't actually typecheck, but you get the idea):
On 10/19/10 2:12 PM, Christopher Done wrote:
Questions (I'm talking about GHC when I refer to compilation):
(1) Are fromString and fromIntegral ran at compile time? I don't think
that this is the case. I think they are just translated to fromString
Hello, World! and fromIntegral 2 verbatim.
(2)
12 matches
Mail list logo
