Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    "However, it is relatively simple to construct example programs which violate global uniqueness of instances in an observable way"
    "Locally, all type class resolution was coherent: in the subset of instances each module had visible, type class resolution could be done unambiguously."
    Jean-Louis Giordano
    @Jell
    oh I see
    if two different modules provide two different type class implementation for the same type but are imported separately
    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.
    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.