## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### Activity
Jean-Louis Giordano
@Jell
ok got it
jolod
@jolod
I guess if D would call a Set method though, then you'd get overlapping definitions?
Or Ord method rather.
Jean-Louis Giordano
@Jell
but then you will probably have required a module that has transitively required the two implementations, then I think you get a compile error? or?
jolod
@jolod
I don't really understand how this works; I just remembered Marco showing me this a couple of years ago and I just found this article by googling. :-)
Jean-Louis Giordano
@Jell
ok I'll dig into it
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.