davean 2017-02-28 17:45:12
go #ghc
Koterpillar 2017-02-28 17:46:12
nshepperd: well, sin undefined <= 1
nshepperd 2017-02-28 17:57:04
fix (\x -> x / 100) would work in a decimal bounded setting (0 < x < 1), then you could do x/100 = 0:0:x
Cale 2017-02-28 17:57:07
Koterpillar: But then the next step gets you, you would presumably want to know that sin (sin undefined) <= sin 1, however, to get that, you need to know something more subtle about the sine function, such as the fact that it's monotonic on [0,1]
Koterpillar 2017-02-28 18:08:16
Cale: if I (somehow) compute sine starting from the most significant digit, then since head (sin undefined) == 0, that gives me a _better_ upper bound on sin (sin undefined)
Cale 2017-02-28 18:09:42
How though?
Cale 2017-02-28 18:09:56
I know that by using arbitrary amounts of analysis you can get that
Cale 2017-02-28 18:12:11
Just knowing that sin (undefined) < 1 doesn't tell you much about sin (sin undefined) unless you know something about sine itself, such as monotonicity in an interval.
Cale 2017-02-28 18:12:47
In particular, without something special, you're not going to obtain sin (sin undefined) < sin 1 like you want
threshold 2017-02-28 18:14:14
Do the integers for a partially ordered set with respect to the order ≤ ?
threshold 2017-02-28 18:14:18
form
Cale 2017-02-28 18:17:30
yes
Cale 2017-02-28 18:17:43
(moreover, they're totally ordered)
pikajude 2017-02-28 18:18:44
duuude
nshepperd 2017-02-28 18:23:12
I think you need to take advantage of one the trigonometric identities involving sin to do this. and to be able to express such identity as a constructor of your real number type
nshepperd 2017-02-28 18:23:40
it seems like it might be possible, but I don't know how
Cale 2017-02-28 18:24:50
Yeah, maybe if you contrived your representation of the reals around the ability to do this :)
Cale 2017-02-28 18:25:43
(i.e. cheating by building in sine-related stuff)
nshepperd 2017-02-28 18:27:27
well, not quite cheating
nshepperd 2017-02-28 18:27:40
I mean, putting in a Sin constructor wouldn't help at all
nshepperd 2017-02-28 18:28:30
I was thinking of continued fractions or something but I don't really know
Cale 2017-02-28 18:28:34
It might help :)
Cale 2017-02-28 18:28:56
(though it would make the implementation of all your operations really annoying)
nshepperd 2017-02-28 18:30:05
show x@(Sin y) | accursedUnutterablePtrEquality x y = "0" -- :)
Koterpillar 2017-02-28 18:32:13
a bounded constructor will help, probably
Koterpillar 2017-02-28 18:32:54
data BReal = ExactValue Float | Between Float Float BReal
Younder 2017-02-28 18:33:52
Quirky ADA :)
nshepperd 2017-02-28 18:34:39
hmm.... a sequence of decreasing bounds, perhaps
nshepperd 2017-02-28 18:34:44
this sounds familiar
Koterpillar 2017-02-28 18:36:05
I thought this was how CReal was implemented anyway?
Cale 2017-02-28 18:36:46
iirc, CReal is implemented as a sequence of rational numbers such that the nth is within 1/2^n of the limit.
nshepperd 2017-02-28 18:37:17
sin x 0 = Between (-1) 1; sin x n = Between { some function of (x (n-1)) }
Cale 2017-02-28 18:37:17
So that effectively gives you a sequence of intervals of decreasing size
Cale 2017-02-28 18:37:53
nshepperd: that first bit is a type error... ;)
Younder 2017-02-28 18:38:19
How are the size and computational properties of CReal?
Cale 2017-02-28 18:38:44
It's fairly impractical
Cale 2017-02-28 18:38:52
It's okay for some things
nshepperd 2017-02-28 18:38:56
Cale: nah, I'm talking about numbers that are functions now
nshepperd 2017-02-28 18:39:05
the Int -> a kind of sequence
Cale 2017-02-28 18:39:35
> sum [1..1000] :: CReal
lambdabot 2017-02-28 18:39:42
mueval-core: Time limit exceeded
Cale 2017-02-28 18:39:49
^^ but it's pretty bad for general computation
Cale 2017-02-28 18:43:32
> exp (pi * sqrt 163) :: CReal
lambdabot 2017-02-28 18:43:36
262537412640768743.9999999999992500725971981856888793538563
Cale 2017-02-28 18:43:46
^^ not that bad so long as the expression is simple
nshepperd 2017-02-28 18:44:33
so in conclusion, I feel like maybe CReal or something like it should be able to do this, but I don't really understand its implementation
nshepperd 2017-02-28 18:44:58
unfortunately sin ⊥ is actually ⊥ in CReal though
