Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    jolod
    @jolod
    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.
    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.