Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
Activity
jolod
@jolod
Nice tag line: "Functions in - fictions out".
Jean-Louis Giordano
@Jell
after reading that article, I also agree with everything in :p
jolod
@jolod
It all looks very good. Does the last point mean that I can use do notation with sets in Idris?
The real problem of why Set is not a monad in Haskell is that it requires Ord. Mathematically there's no issue.
Jean-Louis Giordano
@Jell
not sure how you would go about it, but if you can write a bind + pure function then yes afaik
last time I wrote idris a bit "seriously" was like 2 years go, I'm starting to forget some stuff :p I should get back to it maybe this year :D
so the Set do would kind of behave like a List monad @jolod ?
I can try to do that later today
jolod
@jolod
Yeah. In PureScript I routinely did Set.fromFoldable \$ do ... and in the do I did Array.fromFoldable someSet. Annoying.
(So x <- Array.fromFoldable xs.)
Jean-Louis Giordano
@Jell
there you go @jolod :
module SetMonad
import Data.SortedSet

(>>=) : (Ord a, Ord b) => SortedSet a -> (a -> SortedSet b) -> SortedSet b
(>>=) xs fn = foldr (\elem, accu => union (fn elem) accu) empty xs
pure : Ord a => a -> SortedSet a
pure a = fromList [a]

shenaningans : SortedSet Int
shenaningans = do
a <- fromList [1,2,3]
b <- fromList [1,2,3]
pure (a * b)

result : List Int
result = Data.SortedSet.toList shenaningans
(kind of need to force evaluation on the result with :x at the repl though, my understanding is that do has lazy semantics)
jolod
@jolod
Nice!!!
Erik Svedäng
@eriksvedang
❤️ Idris ❤️
jolod
@jolod
Random question, but does anyone know where the style of very abbreviated function/variable names come from? It seems to be very common in C. I think maybe some old language had a restriction on having one-letter names for things like loop variables or something like that, but C does not have such restriction.
Erik Svedäng
@eriksvedang
Programming on teletypers is what I’ve heard... not sure though, it’s just a natural tendency for a lot of people I think (?)
jolod
@jolod
Maybe it stuck for those that entered BASIC programs from magazines. I imagine that most used rather short variable names. They then carried that over to C and what-not.
Magnus Therning
@magthe
Unique in first 8 characters is a rather strict requirement on length.
jolod
@jolod
@magthe!!!
That explains so much!
jolod
@jolod
Do any of you use any source code formatters for Haskell?
jolod
@jolod
@Jell So does this also mean that in Idris you can have the same name for type constructors?
Jean-Louis Giordano
@Jell
@jolod yes! Lists, Vectors and Heterogeneous Vectors all have the same type constructor names Nil and (::), which also means they can all be represented using the list notation [1,2,3]
Jean-Louis Giordano
@Jell
(did I mention I really like Idris?)
jolod
@jolod
That. Is. Super. Nice!
Magnus Therning
@magthe
Here I thought I looking forward to a short quick stretch to get my Dhall experiment across the finishing line... took the whole day due to safety :/
Erik Svedäng
@eriksvedang
so it's very safe now?
Magnus Therning
@magthe
Haha, well, it's a little bit more complicated now.. is how I'd put it.
Erik Svedäng
@eriksvedang
OK :)
jolod
@jolod
@magthe Sounds like every Haskell beginner/skeptic ever. ;-)
Erik Svedäng
@eriksvedang
when your dialogue scripting language suddenly becomes prolog...
ENTRY {
Is [CHARACTER] [CHARACTER] ? -> ARE_THEY_THE_SAME
}

ARE_THEY_THE_SAME (= arg0 arg1) {
Yes
Yeah!
For sure
}

ARE_THEY_THE_SAME (/= arg0 arg1) {
No
Nope
I don't think so
}
(also, sorry for creating a language that mixes C-style curly brackets and S-expressions :P)
Magnus Therning
@magthe
@jolod to be specific, I have to use two fallbacks on the imports, whereas I first thought I could get away with only one.
jolod
@jolod
@magthe I have no idea what that means. I only have a very high level idea of Dhall. :-)
Magnus Therning
@magthe
Maybe something worth talking about at some point then.
That and Nix.
jolod
@jolod
Defunctionalization is something Clojurists love. It is captured by the "data > functions > macros" mantra.
Jean-Louis Giordano
@Jell
oh I did not realize that!
interesting
The claim is simple: in a static type system, you must declare the shape of data ahead of time, but in a dynamic type system, the type can be, well, dynamic! It sounds self-evident, so much so that Rich Hickey has practically built a speaking career upon its emotional appeal. The only problem is it isn’t true.
jolod
@jolod
@eriksvedang idk, I think any treatment of dynamic vs static is bound to be a failure, since it's comparing one orange to a whole garden of different apple trees. The critique from the dynamic camp is usually implicitly qualified with "[static typing] in a language that I can actually use to solve my problem", and proponents reply (as this blog does) with "sure, language X has some flaws, but look at these 10 different languages that all have one aspect of what you want".
Sorry, the blog only listed 6 languages.
jolod
@jolod
Other than that, the post is relevant, but I do feel that it strawmans a bit (without reading the original replies so I cannot say for sure) but the dynlang camp is usually the worse offenders of strawmanning, so whatever. It anyway over-reaches in the conclusion I think; the two arguments are not sufficient to conclude that statically typed systems (of some flavor) is at least as open and dynamically typed systems. In particular, I'm surprised that he didn't actually deal with the Maybe issue that Rich Hickey raises; he simply dismissed Rich Hickey's critique as "emotional" and "has built a career on". I suppose he would say that it's only about "being upfront with what you require" which misses the point that requirement can change, and then he would, I presume, shift the goal posts and say "sure, in Haskell, but not in these other six languages". On that note, I'm not sure that any of those languages actually solve all the problems that would occur. Most of the time, people argue that in Haskell something is a particular way, and then refer to another language when Haskell isn't perfect, without bringing in the problems that that difference has on other languages. So it's cherry picking the best of all the statically typed languages, which again, doesn't fly for someone that wants to actually program.
Erik Svedäng
@eriksvedang
fair enough :)
jolod
@jolod
@Jell Agree with everything in that post. I particularly like that he points out the "static types vs no static types" issue, e.g. while Python is considered dynamically typed, you usually don't treat typed dynamically.
Maybe it is better to say that a program is dynamically typed (if it indeed e.g. changes the type of an object), rather than using "dynamically typed" as a statement about the language.