Hacker News Reader

Elm's type systems is really constrained compared to PureScript's. It's great for people coming from JavaScript, but not so much for those coming from Haskell.

Also, you still need FFI in Elm. elm-lang/virtual-dom is basically just a wrapper around the native virtual-dom library. Also, afaik there's nothing like react native for virtual-dom.

pkaon Hacker-Proof Code Confirmed

> What you are doing is claiming types into and out of functions decide if they are functioning correctly. This is not the case at all.

When I say proof, I mean it in the mathematical sense. The Curry–Howard isomorphism [0] formalizes the relationship between (mathematical) logic and type theory. Unless you are saying mathematical logic is inconsistent (and thus every mathematical proof is invalid) this is absolutely the case.

The same way you can construct a mathematical proof that e.g. n is prime, you can can construct a type Prime n that proves that n is prime [1].

> I think that most bugs aren't because the type you were expecting was wrong but the data produced by a function was wrong.

This is where your misunderstanding stems from. Continuing with the example from above, if you have a function:

    makePrime :: n -> Prime n

the function can not construct (Prime n) if n is not a prime.

> If I call `get_lottery_number` by your logic it will always provide me with the real winning lottery number since the types check out. That is absolutely incorrect. Types can't prove functionality.

If you give me a specification that constructs predicted lottery numbers I could absolutely turn it into a type :)

> They do provide protection from a set of bugs but those bugs are also avoided easily by handling every case

But you don't have proof that you are handling every case :)

> You can't say a program will have no bugs because the types check out. Is that what you are saying?

Yes, if the types correspond to the specification then there are no bugs. The specification can still have bugs though, but that's unavoidable. The thing is that you've proven the program does what you told it to do.

Once you stop thinking about types in the Java sense and start thinking about them as logical propositions it will all make sense. I provided you with a couple of links in the other comments and here if you are still interested.

[0] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[1] https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat...

pkaon Hacker-Proof Code Confirmed

> This is wrong because it depends on the language. The behavior depends on the implementation but if you are meant to return the first character in the string and the string has no characters then you should return an empty string if provided a string with no characters.

How? The type is:

    takeFirstChar :: String -> Char

There's no such thing as an empty char. Your get_first_letter essentially has the type:

    get_first_letter :: Either Null String -> Either Null String

Which doesn't guarantee anything and is arguably a lot worse than just:

    get_first_letter :: NonEmptyString -> Char

This is why you can't have proven code in a lot of languages, because they permit you to lie about the actual types. From there, any proof is invalid because it is based on invalid propositions.

Dependently typed and other languages do not allow you to lie about the types (for example, a value can't be null unless this is reflected in the type; you can't throw exceptions or do IO unless this is reflected in the type, etc), hence a well typed program in such a language is a valid proof. You can not implicitly cast between types, i.e. a function like:

    cast :: a -> b

doesn't exist.

A function like print actually has the type:

    print :: String -> IO ()

Which tells you that it is doing IO. You can't call such a function from a pure function for example, the types wouldn't permit it.

> Also, you are assuming the implementation of neString is correct. What if that has a bug? Again, just because your passing your data around the correct way doesn't mean the correct things are happening with it.

I was simplifying, but neString would actually have a type similar to:

    neString :: String n -> Maybe (String (n != 0))

where n is the length of the string. Notice, the length is encoded in the type! A wrong implementation (one that returns i.e. Maybe (String 0)) will not type check.

But yes, you can have errors in your proof, no doubt. But these are specification errors, which there's no way to get around. What a proof guarantees is that there are no errors in the implementation of your specification.

pkaon My Most Important Project Was a Bytecode Interpreter

I'm thinking a lot of the complexity of writing a compiler stems from the usage of inappropriate tools. I.e. I would rather kill myself than write a lexer in C (without yacc / bison), but using parser combinators it's a rather trivial task.

Similarly, annotating, transforming, folding, pattern matching on, CPS transforming etc. the produced AST is pretty trivial in a language that supports these constructs. And again, a nightmare in C.

That leaves codegen, but using the right abstractions it turns into a very manageable task as well.

Here's a compiler written in Haskell for LLVM [0].

[0] http://www.stephendiehl.com/llvm

pkaon Hacker-Proof Code Confirmed

Well, an F to C converter is not a terribly interesting case, because it would be trivial to implement. When you think about it, how would you test this in your favourite language of choice? By computing the expected value by using the same formula you used to compute the value you are testing in the first place.

But here's another example that came up recently. Let's say you want to write a function that takes a string and returns its first character. Now, it would be an error to call this function with an empty string, because then what would it return?

In a normal language, you'd probably check if the string was empty and then return null or something. When testing the function, you'd have to remember the empty string case and write an unit test for it (now I don't know about you, but I can't say I'd always remember to write a test case for this particular edge case; normally I'd forget).

Can we do better? It turns out we can.

We can encode invariants about our program on the type level. Types can be more than just strings, ints and chars. They can also be propositions, i.e. statements about our program. In this particular case we can construct a type

    NonEmptyString

that can only be constructed by a function like this (using Haskell syntax):

    neString :: String -> Maybe NonEmptyString

(This means that neString takes a String and returns a Maybe NonEmptyString). But what is this Maybe (also called Option, etc)?

It's like a union type - it can either contain some value, or it must be empty. Now the cool thing about Maybe is that we can't just take out the potential value contained inside it - we have to pattern match on it! What this means is, that whenever you want to see what's inside a Maybe the compiler forces you to tell it what to do in both cases - when there's something inside and when there's nothing inside.

Maybe you can see where this is going. This is how our takeFirstChar function would look like:

    takeFirstChar :: NonEmptyString -> Char

Notice - we say that it only works on NonEmptyStrings! If we try to pass a regular string to it that would be a compiler error. But now we want to read something from the command line and returns it's first char. Let's say we have a read function:

    read :: String

Every time you call this function it gives you a string read from the terminal. Ok, let's put our program together now:

    a = read
    print (takeFirstChar a)

But wait! We can't do that - as I said above, the compiler complains, because we try to pass a String to a function that expects a NonEmptyString. Instead we have to:

    a = read
    case (neString a)
      Just st: print (takeFirstChar st)
      Nothing: print "String was empty"

Notice how we pattern match on the result of (neString a). If the string was empty, we'd match the Nothing clause. In all other cases we'd print the first char.

What we did is prove that the program will behave correctly in all cases - no tests needed! We can't put the program together in any other way, because it would be a type error. In a sense, the fact that the program exists is a proof of its type (programs have types too!)

Now this is a pretty trivial invariant to encode on the type level, but in a dependently typed language you could encode whatever you'd like, i.e. for example that a list is sorted or that a number is the GCD of two other numbers, etc.

This is often not trivial to do, and at some point you start seeing diminishing returns, because the time it takes to rigorously encode a proof is longer than any possible return of investment caused by proving that there are no bugs. But doesn't have to be an either-or situation. You can encode as much invariants as you'd want in your code. I think Haskell strikes a good balance in that regard, although Idris is a very interesting language too.

(Sorry for typos, errors etc, didn't proofread).

pkaon Hacker-Proof Code Confirmed

> Also, you know as well as I do that you don't need to test every input, only a representative subset if you use unit tests and use a fuzzing testing library.

The thing is that you can never be sure that you chose a "representative subset". Unless you test every conceivable input you've verified that your program works for the subset you chose to test, nothing more. For example, how sure are you that your unit tests cover every conceivable edge case?

> How do I go about defining a test using a formal method?

You don't, it's a proof. You don't need tests.

Some links from another comment [0].

I'd also point you to Idris [1] for a friendly dependently typed language if you are interested in learning more.

[0] https://news.ycombinator.com/item?id=12544477

[1] http://www.idris-lang.org

pkaon Hacker-Proof Code Confirmed

Exactly :) And a proof that the spec is correct.

But without formal verification both your spec and the implementation may be incorrect.

pkaon Hacker-Proof Code Confirmed

    - Unit testing: Provide every test case possible

Even if your program only takes a 32 bit integer as an input you'd have to provide 4294967296 test cases. Most programs' inputs are a bit larger than that.

    - Pure Functions: Use small methods that cannot error and always return sane values

"cannot error" is exactly what formal verification is about. Pureness doesn't prove correctness.

   - Fuzzing Testing: To find if the implementation is actually correct or if it is correct by chance

Fuzz testing is good for finding buffer overflows and such, and those bugs can be ruled out even without formal verification methods (i.e. Rust). Otherwise you'd need to specify every test output possible anyway, and you're back to point 1.

pkaon Learning from Ada

The sibling comment points out property based testing (see QuickCheck), which is a good idea in any language. And yes - you don't need to write that many unit tests (but still some) when using a type system, because you can encode a lot of invariants in the types.

But still, my point stands - writing tests during early experimentation is a lot harder than just altering some type and letting the compiler infere what needs to be done or what you broke.

I've spent some time writing Clojure and still use dynamic languages a lot for smaller tasks, so I know both sides. This doesn't mean much, but I'd really encourage you to try some ML language and spend some time with a nice type system. Haskell is probably too big a time investment, so maybe try Elm [0] - it's very beginner friendly and a lot of the people using it come from JavaScript.

[0] http://elm-lang.org

pkaon Pitfalls in Haskell

Yes, record accessors being partial functions is a big problem.

One way to deal with this is to not use fields at all together with algebraic data types (i.e. when you have more than one constructor), just pattern match. When you have some common field across all constructors, define a regular function to pull it out:

    someData :: MyData -> a

and use that instead. As to the second use case, if you need to access something common to A and B but not C, then:

    someOtherData :: MyData -> Maybe a

and pattern match on that. Or first pattern match on C and then have a catch all _ for A and B.

lens remedies a lot of Haskell's pain points when it comes to records, but I have to say that PureScripts record system is so much nicer.

pkaon Learning from Ada

While I disagree (static typing is much more than catching type conversion errors), my point was that it makes experimentation and design exploration much easier and faster. Without types, you'd need mock data for even the simplest of programs, and changing mock data structure is much more painful than changing a type somewhere and getting the places (all the places) where your program turns then out to be incoherent. Not to mention that types are much more than Persons or Gorillas, they can be higher order functions too (Person -> Gorilla) that are passed around.

pkaon Learning from Ada

I'm not an expert on type systems, but I don't think it would add that much in your case. You might get more out of it if you wanted by using phantom types, which is just a way to differentiate among structurally identical types, like this:

    reduceGraph :: Graph a -> Graph Reduced

Now you can't pass unreduced graphs to functions where you expect some sort of an already reduced graph, and you could encode as much invariants as you wanted in your types, but yea, in cases where there are homogenous types with little variance (machine learning, statistics, your use case) static typing won't probably bring that much (unless you go nuts with dependant typing I guess).

pkaon Learning from Ada

Agreed. My comment wasn't aimed that much at Haskell in particular (even if it's my language of choice), but rather the idea of using structure/types for fast experimentation, rather than just a REPL.

Also, using a type checker to wholly check your Lisp code basically makes it a static language, the difference then is pretty much philosophical I'd say.

pkaon Learning from Ada

Static languages, in particular Haskell, PureScript, etc, are unparalleled when it comes to fast prototyping or design space exploration. The compiler can show you whether your idea even makes sense before writing big chunks of business code.

How? By building the structure/hard stuff first and letting the compiler verify it while leaving out the uninteresting parts.

A very simple example. Let's say you have some data model with people, addresses, whatever. You want to see what you need to do to get a list of addresses for some group of people.

You start by defining the structure of your data model (this can depend on DB schema, business requirements, whatever):

    data Person = Person { name :: String, city :: String }

    data Address = Address { city :: String, zipcode :: String, street :: String }

Now, go straight to the hard part. No need to fuck around with DB connections, mock data, whatever:

    getAddresses :: [Person] -> [Address]
    getAddresses = undefined

Leave out the implementation for now. So probably we are gonna need a way to get an Address for a Person. Ok:

    addressForPerson :: Person -> Address
    addressForPerson = undefined

Again, leave out the implementation. Now go back to `getAddresses` and see if we can implement it now:

    getAddresses = map addressForPerson

Cool, the compiler doesn't complain. So far we've verified that if we have a function like `addressForPerson` we can safely assume that our design is going to work.

Now we can go back to `addressForPerson` and implement that. But turns out, we only have a city stored in Person, so the best we can do is get back a list of potential addresses for each person. So we need to adjust that type signature:

    addressForPerson :: Person -> [Address]
    addressForPerson = undefined

Leave out implementation, it's trivial so no need to spend time on it now. But now the compiler complains that `getAddresses` doesn't make sense anymore! We are saying that, having a list of people, we can get a list of addresses, but that's not true anymore. We found out that we can only get a list of potential addresses, so we have to adjust the type signature.

    getAddresses :: [Person] -> [[Address]]

Now every use of `getAddresses` will have to be adjusted to the new requirements. Etc etc.

Granted, this is a very simple example, but I hope it illustrates how static languages facilitate extremely fast prototyping. Sure, a Lisp REPL is very very nice, but in my personal experience it's no match for a type system. We didn't even have to mock data to start experimenting!

(And yes, Haskell, OCaml, PureScript, Elm etc all have a REPL too).

pkaon Climbing the infinite ladder of abstraction

I just really hope I’m not wasting my time.

I think this is very easy verify: just climb down the abstraction ladder and try to solve some particular problem without those abstractions. If you then find yourself yearning for monads, macros or whatever else, then no - you haven't.

One particular thing that stuck with me during the past few months was the continuation monad/coroutines abstraction PureScript's Thermite library is built on. I happened to work on a project with another colleague, we were both writing some UI stuff and while he was fighting with callback hell I was happily writing sequentially looking code in the Aff monad.

It's not a particularly heavy abstraction, but something that can make your life so much easier. Most abstractions I use tend to fall into that uhm... category :)

pkaon React: Mixins Considered Harmful

On the contrary, it's about reducing complexity. You don't have to worry about mixins, classes, prototypes, inhertiance. Just plain old functions. Can't get simpler than that.

pkaon React: Mixins Considered Harmful

Higher order functions are not such a complicated concept. Just a function passed to a function.

You use functions, right?

pkaon React: Mixins Considered Harmful

No no, just higher order functions. They don't have join and return.

pkaon What’s Next for Artificial Intelligence

I'm not qualified enough to comment on the possibility of strong AI, but one thing to consider is that natural intelligences don't launch the missiles only because they are afraid of the resulting total annihilation, of death basically. Maybe globally distributed strong AIs won't have such concerns.

pkaon Learning Elm has gotten me confused about static vs. dynamic typing

For all I know

Agreed.

pkaon Faithful Elm and the Amazing Router

Look no further! Try Purescript. It's basically Haskell (albeit strictly evaluated) and has everything you listed, plus a record system I really wish Haskell would adopt.

I'm currently using it in production with purescript-thermite, a thin wrapper over React, and it's worked out great.

Elm is great for people coming from JS, but not so much for people coming from Haskell.

pkaon Learning Elm has gotten me confused about static vs. dynamic typing

There [0]: the GCD m n d type proves that the greatest common divisor of m and n is d.

[0] http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.a...

pkaon Learning Elm has gotten me confused about static vs. dynamic typing

As I said above, you can verify/prove the invariants you capture in the types. I don't know what you mean by "correctness of loops", but if you capture whatever it means in a particular type, yes you can.

If you really wanted, you could derive a proof that pi is equivalent to some sort of corecursive series, which you can then evaluate in a dependently typed language, I guess. A proof is a type.

On the other hand, how would you write a unit test that checks whether something calculates pi without comparing its result to pi itself?

pkaon Learning Elm has gotten me confused about static vs. dynamic typing

But if it compiles its status is not unknown. It means it is well typed, proving the absence of a whole lot of bugs.

Generally, refactoring in dynamic languages without tests or something like Clojure's schema is madness. Usually not a problem in strongly typed languages, even without much test coverage.