4 ms·
> Pattern matching for one. I can prove that 3 cases won’t be met but I have to ‘fill in’ them anyway. >> This is a funny one because, no, GHC will not ask you
by wellpast 7y ago
> Pattern matching for one. I can prove that 3 cases won’t be met but I have to ‘fill in’ them anyway.
>> This is a funny one because, no, GHC will not ask you to fill them in! You have to turn on a warning for it to complain. The fact that the warning is not on by default is one of my pet peeves with GHC!
Okay, so let's do the inverse then. I've got a pattern matched case that the type prover proves will never occur (so it throws type error) but I want it to occur.
The answer I know is obvious: I have to add it to the type union. But it should be obvious at this point that the moves I am making are not driven by the outcome I want but by the rules of the type checker. At some point you have to say, Why am I playing these games? Do they really yield tangible, business-facing value?
> ADTs with non-Maybe fields. I can prove that all is fine if this ‘slot’ isn’t filled in.
>>Another funny one, because you can just use `undefined` or `error` and GHC won't complain! Personally I'd probably prefer that it did.
But I don't want an error. I can prove that the absence of the field is OK/not-an-error.
If you say then make it a Maybe, I will tell you sorry I don't have the time to update my entire code-base to contend w/ this novelty to the type checker (I say to the type checker, but this is never a novelty to me and my dynamic code).
> Trying to pass an opaque reference down a function call chain.
>> I don't even know what you mean by that.
my value --(flows at runtime through)--> [some framework, say a web framework code to a, say, a Label that has no idea about my value's type domain] --(flows through pixels to)--> user's eyes
- tome 7y agoIt's really interesting because I hear these kinds of claims a lot from Clojure programmers. How did they arise in the community? I find it hard to believe that so many Clojure programmers have actually tried Haskell and come to exactly the same conclusion. Does Rich Hickey repeat these points somewhere? If so could you point me to where? I'd love to see them. I'm a big fan of Are We There Yet, Simple Made Easy etc. and find Haskell a great implementation of them. > I have to add it to the type union. But it should be obvious at this point that the moves I am making are not driven by the outcome I want but by the rules of the type checker. That's not how I see it at all. I wish I could understand why you do see it that way! > But I don't want an error. I can prove that the absence of the field is OK/not-an-error. You misunderstand. If you know that a field of a data type is going to be unused you can fill it in with an `error` call that you know will never be hit. You can even omit the field entirely! That's considered bad form but if you like it then knock yourself out. data Foo = Foo { bar :: Int , baz :: String , quux :: Bool } doSomething :: Foo -> IO () doSomething foo = do print (bar foo) print (baz foo) example1 = Foo { bar = 42 , baz = "Hello" , quux = error "quux will never be inspected" } -- > doSomething example1 -- 42 -- "Hello" example2 = Foo { bar = 42 , baz = "Hello" } -- > doSomething example2 -- 42 -- "Hello" > my value --(flows at runtime through)--> [some framework, say a web framework code to a, say, a Label that has no idea about my value's type domain] --(flows through pixels to)--> user's eyes What's wrong with a polymorphic parameter?
- wellpast 7y agoWhat I find crazy about these conversations is that I will say “I don’t like that I have to do X...” And the response is always “But that’s easy you just do X...” The argument is not that you can’t do some task in Haskell. With enough time you can do anything in any language. That’s the given. The argument is I want throughput. If I’m doing X I want to do it because it is necessary to the problem solution. This is why you hear these laments from Clojure programmers. Because when we code we are doing the minimal amount of work to produce correct programs. Strongly typed systems add fanfare that Clojure programmers have found no need for.
- tome 7y agoThank you for your response. I'm afraid I don't understand. Your point seems backwards. On the specific point in question you said (paraphrasing) you don't like filling in a field of an ADT if you can prove it's not used. I pointed out that in Haskell you indeed need not fill it in. You said (paraphrasing) you don't like matching on a constructor if you can prove it's not used. I pointed out that in Haskell you indeed need not match on it. You don't want to do X. I'm telling you that you don't need to do X! Anyway, I'm more interested in the general point. Where do Clojurians get these ideas about Haskell? Are there specific blog posts or videos you can point me too? I'd rather confront the general case than specific instances buried deep down in forum threads.
- wellpast 7y agoThanks for your reply, as well. But there’s no indoctrination going on. It’s right there: > If you know that a field of a data type is going to be unused you can fill it in with an `error` I don’t want to fill anything in. I don’t want to have to tell the checker what I know and the world already knows just because it thinks it needs to know it. There’s no indoctrination. We don’t have to “fill in” anything in Clojure. I wonder sometimes if this is a thing where you can’t see the air because it’s all around you? In static-type space you are (by definition) a slave to the type checker. Sometimes static-type enthusiasts will say they lean on the checker, it helps them. But I have a weird sense that this is a kind of Stockholm Syndrome. Sorry I’m a bit caustic sometimes, but it’s all good natured I promise - the hope is it draws out a point that will prove me wrong. You clearly know your domain well, and I appreciate the back & forth. But I do stand by my position (until knocked out of it.)