`Stream a` doesn't implement `(RealFrac a) => RealFrac (Stream a)` about copilot HOT 6 CLOSED

Trying to propose a PR. But there's a restriction on Cast right now:

Cast :: (Integral a, Num b) => Type a -> Type b -> Op1 a b

Either this Integral constraint will have to be removed, or a new cast operator will have to be adder for floating-point values. @leepike do you have an idea?

from copilot.

Yves,

It's been a while since these design decisions were made, but I think I

remember we decided to disallow some of these unsafe casts, but Lee
probably remembers the details as to why better.

On Tue, May 17, 2016 at 5:53 PM, Yves Parès (Ywen) <[email protected]

wrote:

Trying to propose a PR. But there's a restriction on Cast right now:

Cast :: (Integral a, Num b) => Type a -> Type b -> Op1 a b

Either this will have to be removed, or a new cast operator will have to
be adder for floating-point values. @leepike https://github.com/leepike
do you have an idea?

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly or view it on GitHub
#4 (comment)

Alwyn E. Goodloe, Ph.D.
[email protected]

Research Computer Engineer
NASA Langley Research Center

from copilot.

@agoodloe Actually, I think that the fact that the unsafe casts are disallowed is pretty sensible.
The problem is that the RealFrac functions are unavailable. (And they seem to be unavailable in Atom too...)

from copilot.

Yves,

You are correct the back ends are a constraint.

Gorges-Axel who did a lot of work last summer on Copilot -->SBV sent me

a note reminding me that

From what I remember, I did not implemented the cast float -> int because
of the sbv backend.

We have the promotion from integers to IEEE 974 by using "S.toSDouble
S.sRoundNearestTiesToEven", but I do not know if there is something
similar to go the other way. If there is, then it can be (almost) easily
implemented.

If there is no way to get it back, the best way remains calling an
external function that will do the cast in C, but you will loose all the
model checking power of SBV.

On Tue, May 17, 2016 at 6:34 PM, Yves Parès (Ywen) <[email protected]

wrote:

@agoodloe https://github.com/agoodloe Actually, I think that the fact
that the unsafe casts is pretty sensible.
The problem is that the RealFrac functions are unavailable. (And they seem
to be unavailable in Atom too...)

—
You are receiving this because you were mentioned.
Reply to this email directly or view it on GitHub
#4 (comment)

Alwyn E. Goodloe, Ph.D.
[email protected]

Research Computer Engineer
NASA Langley Research Center

from copilot.

I know that this is old. We are looking into making some small changes and cleaning copilot overall, and we just discussed this.

In my opinion, it cannot be done. The interface of RealFrac is too permissive. Recall that:

class  (Real a, Fractional a) => RealFrac a  where
    properFraction   :: (Integral b) => a -> (b,a)
    truncate, round  :: (Integral b) => a -> b
    ceiling, floor   :: (Integral b) => a -> b

If you allow this, then you could try to floor a stream of Floats into a stream of Integers, since the floor operation is polymorphic on the b. But we do not support unbounded ints in Copilot.

But it gets worse: I should be able to floor a stream of Floats into one single Int, as in:

aStream :: Stream Float
aStream = ... --defined in some magical way

myNumber :: Int
myNumber = floor aStream

Obviously this does not make sense. RealFrac is too permissive. I think what needs to happen is that we support numeric operations to produce code as simple as you need it, but without using the actual RealFrac class.

from copilot.

Hey folks, just checking in here.

I think what needs to happen is that we support numeric operations to produce code as simple as you need it, but without using the actual RealFrac class.

Is there any movement in this area?

I'm perfectly fine with some combinators floating around outside of the RealFrac class. I have some use-cases where I very much need to floor a Stream Float; and I'm okay with accepting the burden of unsafety it brings with it with regard to overflows 😄

from copilot.