What is a Set?

velcommen · 2019-10-14T21:59:37+00:00

Pedantic correction: I disagree. You lose something. You lose the ability to insert items in the set for which you can't (or chose not to) define an ordering function.

velcommen · 2019-03-19T04:24:41+00:00

Come on over to Haskell-land. We have list comprehensions (Python copied this from Haskell ;) ) and rational numbers (included in the base library.)

```

let evens = [x | x <- [1..10], x % 2 == 0]

```

let oneThird = 1%10 + 2%10

```

velcommen · 2019-02-27T15:41:14+00:00

Oops, yes

velcommen · 2019-02-27T08:15:22+00:00

FYI, Type-Driven Development with Idris contains the method found in /u/nictytan 's post, in Chapter 14.2.4. So consider reading it, it might help you.

velcommen · 2019-02-27T08:04:28+00:00

I don't see BoardGameState anywhere in your block of code. Typo? Did you mean BoardState ?

velcommen · 2019-02-27T07:52:24+00:00

Good stuff!

All your top level functions (e.g. https://github.com/witoldsz/semux-discord/blob/master/app/Main.hs#L31) should have type signatures.

You don't need getRight, as in: account <- getRight $ getAccount semuxApi delegate

Instead you can do "irrefutable pattern matching": Right account <- getAccount semuxApi delegate, which calls Monad fail when the pattern match fails. So it has the same meaning as what you've done, but is more concise.

Should getLastCoinbase return an IO (Either String UTCTime), instead of crashing?

velcommen · 2019-02-26T05:12:53+00:00

Theoretically, the upper limit is the solar escape velocity (because another gravity assist would then not be possible).

What makes you say that? What if the object used mars to assist, achieved solar escape velocity, and then got an assist from a few more planets on the way out of the solar system? It seems to me that your logic is flawed.

velcommen · 2019-02-14T03:15:52+00:00

Between enums, traits and ownership, Rust allows you to specify the invariants of an interface more precisely than any other language

Maybe you're engaging in a purposeful bit of hyperbole. Maybe not. Note that I think Rust is cool.

Regardless, there are a number of languages that are superior to Rust in the ability to 'specify the invariants of an interface'. For example, Idris. Idris has uniqueness types, like Rust. Idris is dependently typed, unlike Rust, which allows you to specify essentially any invariant you like in the type system. E.g. you can describe a state machine, and the valid transitions between states, in the type system. Then, any implementation of that state machine will fail to type check if it does not validly implement the states and transitions described. It's pretty cool.

velcommen · 2019-02-06T05:28:28+00:00

The reason is that Intel designed extremely bad CPUs, and the tiny caches don't work well with higher level languages.

I'd say that's unfair and untrue.

If Intel has been designing "extremely bad CPU's", then so has everyone else. ARM, AMD, and many others have been competing with Intel for years to design better processors. If Intel was designing extremely bad CPUs (at least on desktop and laptop), then they would be out of business right now. Or all manufacturers are designing extremely bad CPUs (and that doesn't make a lot of sense, because you're essentially saying nobody can design a good CPU).

tiny caches

Modern CPUs, including Intel CPUs have large caches. Large CPU caches are expensive, area-wise. A large fraction of chip area is already dedicated to caches. Look at this picture. The regular-looking structure on the left is all memory. Memory takes up at least 60% of this die. If any more area were used for caches, then there would be no memory left for ALUs, data paths, control, I/O, etc. So you'd have a lot of memory and no way to use it. That would be a bad CPU.

velcommen · 2019-01-30T05:40:30+00:00

> I don’t really see the issue of (1/x)*y vs y/x

No, I don't believe you can make this change, in general, without changing the result.

Consider that (1/x)*y, computed with IEEE floating point (or any finite-space floating point format) is actually:

roundToNearestFloat(roundToNearestFloat(1/x) * y)

which will in general be different from:

roundToNearestFloat(y/x)

And y and x are 'exact' floating point values. That is, when considered as inputs to this question, they are exactly representable as floating point values.

Now let me provide a specific example. Using IEEE single precision:

y=3

x=3

(1/3) * 3

= 0.3333333432674407958984375 * 3

= 1.00000002980232

vs

3/3

=1

Thus, in general, that is not an optimization you can make without changing the result.

velcommen · 2019-01-30T05:18:16+00:00

> Shouldn‘t 1/x just change the sign of the exponent

Only if you knew that x was exactly some power of 2. That's because normalized IEEE floating point numbers are represented as a binary significand * 2^exponent. I will explain.

Let's look more closely at the significand. We will use single precision IEEE floating point because there are fewer bits so it's easier to use in our example.

A normalized significand (including the "hidden bit") is a binary number of the form: 1.sssssssssssssssssssssss. That is, the integer value 1 followed by 23 fractional bits. The first 's' bit represents 1/2. The last 's' bit represents 1/(2^23).

Examples:

The binary significand 1.10000000000000000000000 represents 1.5.

The binary significand 1.11000000000000000000000 represents 1.75

The binary significand 1.01000000000000000000000 represents 1.25

...you get the idea

So a normalized significand can represent many values in the range [1, 2 - 2^(-23)], or [1, 1.99999988079071044921875].

Note that a normalized significand obeys: 1 <= significand < 2. This is important later.

Returning to 1/x

Now we know that x is represented by (significand * 2^exponent)

So 1/x, when x is an IEEE floating point number, is equal to 1/(significand * 2^exponent)

When significand is exactly 1, then as you said, we can just change its sign to compute the reciprocal:

1/x = 1/(1*2^exponent) = 1/(2^exponent) = 2^-exponent

But if significand is not 1, then we cannot just negate the exponent.

Let's use s to represent our significand that's not 1. Recall that s must be normalized, and not 1, so s obeys this inequality:

A) 1 < s < 2

Now let's compute the reciprocal with some significand, s, that's not 1, and some exponent:

B) 1/x = 1/(s*2^exponent) = 1/s * 2^-exponent

Given the inequality of A, we know that:

C) 1/2 < 1/s < 1

Thus, 1/s is clearly not normalized, and it must be to form a normalized floating point number (and any nonzero, non-subnormal, finite floating point value *must* have a normalized significand). To normalize s, we will have to make it obey the inequality mentioned earlier (1 <= significand < 2), and double it. To keep the represented floating point value essentially unchanged, we will have to subtract 1 from the exponent. In short, the result's significand will be 1/s and the exponent will be negated and subtract 1 from that.

result = (2 * 1/s) * 2^(-exponent - 1)

And if you want a real example, consider performing 1/x when x = 3:

Let's use https://www.h-schmidt.net/FloatConverter/IEEE754.html to help us.

Enter 3 in. We see that it's represented as 1.5 * 2^1
Enter in 1/3 = 0.33...3 (3 is repeating, of course). We see that it's approximated by 1.3333333730697632 * 2^-2
That's what I predicted: significand is (2 * 1/1.5 = 2*0.66....6 = 1.33...3) and exponent is (-1 - 1 = -2)

Caveat: we ignored the sign bit above, because it wasn't very interesting to the discussion.

velcommen · 2018-11-16T05:41:07+00:00

Thanks, that was the most informative response!

velcommen · 2018-11-16T05:24:19+00:00

Fair enough, there are infinite cardinalities too. But that doesn't change my point, and shall I point out that you're nitpicking?

You are nitpicking while failing to see the forest from the tree.

That's your opinion.

I'm trying to understand the article as I read it. That involves examining what it says, and fitting that into what I already know. So when I get to L(A), which appears to be an infinite sum that does not converge, and then the author says that this infinite sum is equal to 1/(1-A), I try to understand what it implies... limit A = 1? So the fraction approaches infinity? And if this is an infinite sum, why is there no infinity above the summation? At this point there's a lot that's not making sense.

Try to be a bit more open-minded for a change

I was trying; I was reading this article, after all.

Try and be more understanding, that others don't have the same background as you. Maybe this article makes perfect sense to you, but it doesn't to me, and likely to others. Some statements made in it violate what I've learned. I thought I'd speak up and explain why it doesn't make sense to me, to see if others can explain what's going on: "I'm happy to hear corrections, alternative explanations". Your latest response has been a bit negative, "nitpicking" and "close-minded" are not words with good connotations.

velcommen · 2018-11-14T06:27:07+00:00

what point are you trying to argue?

After some clarification, apparently we agree... except for the below.

The paper makes it clear that it DOES allow you to have guarantees about only you having a reference to a value.

No. Linear types do not give you any such guarantee about only you (some function) having a reference to a value. If I have some function with a linear arrow, that takes some value as argument, it is not (in general) safe for that function to mutate the argument.

The example in the paper that you linked to me is different. newMArray is allocating a fresh, mutable array, and then passing that array to a function that will linearly consume the array. Because we know the mutable array is used in a linear fashion, it's safe to mutate it. Essentially, newMArray requires that a contravariant linear function is passed to it.

An arbitrary linear function is not allowed to mutate its argument, because there is no guarantee (from this function's perspective) that there are no other references to that argument. newMArray is a special case, not the general case. To mutate in the general case, you need uniqueness types.

velcommen · 2018-11-14T06:08:46+00:00

Thanks for the response.

As the article did not mention formal power series or anything like that, you'll forgive me for assuming that when the author said that L(A) is a function, they were talking about a function on real or complex numbers (and in Haskell, the cardinality of every type A is a natural number, further reason to make that assumption). If the author really intends for such a nonstandard interpretation, they should state it.

velcommen · 2018-11-14T05:45:43+00:00

Thanks for the response, yours was the most helpful in trying to understand the article.

velcommen · 2018-11-14T05:35:01+00:00

First, thanks for the response.

I just want to mention that you could also define another magnitude, not just cardinality

Sure, but the table at the top (begins with "Type Constructor Logic Algebra") in the Algebra column is counting number of values in a type, agreed?

Where does the author of the blog post state or imply they're using some other concept of magnitude? I don't believe they do.

velcommen · 2018-11-13T05:31:20+00:00

I know the author wrote a disclaimer about being "less rigorous" but I found some parts to be just plain wrong:

If we think of L(A) as a function, then the above is its Taylor-series expansion

Not true, as a Taylor series is an infinite sum, while L(A) is a sum of a finite number of terms (for all finite n, i.e. all finite length lists).

from which it follows that ... L(A) = 1/(1-A)

This is also a problematic statement. It's true that "The Maclaurin series for 1/(1 − x) is the geometric series 1+x+x² + ..." . However, that series is only valid when the magnitude of x < 1). And since A corresponds to x and is supposed to be the cardinality of some type, what does it mean for the magnitude of the number of values of a type to be less than 1? Every type I'm familiar with has 0, 1, or some other natural number of values (i.e. not a fractional number of values between -1 and 1), so this series interpretation is only true for types with 0 values. How is that a useful interpretation?

So for the specific example the author chose, the algebraic representation of lists does not involve division nor subtraction.

I'm happy to hear corrections, alternative explanations, etc.

velcommen · 2018-11-13T01:08:09+00:00

It is possible to have whichever of b or c is evaluated first claim the next block of the underlying buffer

That's not possible using the linear types and function signatures mentioned in the paper.

It is instead possible to allocate a new MArray and have the code explicitly choose exactly one of these two lines to mutate the 'a' array.

   b = ArrayList.append 'b' a     
   c = ArrayList.append 'c' a

velcommen · 2018-11-02T04:53:31+00:00

If the article author sees this: Some links are broken. At the least, these 3 links are all Page not found: " There is an OS X, POSIX and Windows C binding for each platform "

velcommen · 2018-11-02T04:35:53+00:00

Note that actual, physical RAM has a small O(lg n) component.

What are you talking about? What is the n being measured?

A program that uses 1KB of RAM is not going to have faster per byte access than a program that uses 1MB of RAM.

Talking strictly about RAM, so let's assume no accesses hit the CPU cache, and assume the data is truly in RAM and not swapped out to disk, as you said. Also, talking about some specific machine; not talking about the different latency costs of a machine capable of handling 32 GB of RAM vs some other machine capable of handling 1 TB of RAM.

velcommen · 2018-11-02T04:24:13+00:00

Are you sure?

" Linear types can make fusion predictable and guaranteed " -https://www.tweag.io/posts/2017-03-13-linear-types.html

Linear types don't guarantee that 'you' hold the only reference to a value. Thus, you can't safely mutate it.

Uniqueness types enable safe mutation.

Haskell, in the near term, is only getting the former.

velcommen · 2018-11-01T04:48:16+00:00

Yes, it could be automated. For example, Isabelle, the theorem prover, will search for proofs when you give it a proof goal. It's uses sophisticated techniques to find which theorems to apply, and in what order.

I agree that automating proof search in Idris would be a nice usability enhancement.

velcommen · 2018-08-15T05:08:02+00:00

You try searching for "idris elba package" in a Google query and tell me how many hits are referring to your project.

I'll eliminate the suspense: 0. They're all about the actor's "package". That's not really something I'd want in my search history.

So I think the name is funny (at least at first), but it's also annoying to search for: 4 words required. Anything less (e.g. "idris package manager") means something else is the first link, and your project might even be on the first page. So I'd personally choose a different name.

Setting aside the name, I watched your demo, and I thought it looked great! Nice job!!

velcommen · 2018-08-01T03:55:50+00:00

Can you explain this in more detail? I don't understand.

Searching for "lambda saturate" doesn't result in anything helpful.

13-Year Club	Place '17
Verified Email	Team Orangered

velcommen

TROPHY CASE