Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    Jean-Louis Giordano
    @Jell
    something like that
    overloading is less constraining
    jolod
    @jolod
    Still not sure what you mean by that. :-)
    Jean-Louis Giordano
    @Jell
    you don't have to define a common interface to overload something?
    jolod
    @jolod
    Oh, I see.
    How does resolution work though? Could you show an example?
    Jean-Louis Giordano
    @Jell
    I would need to look it up, also not sure how much of that is only useable in the context of dependent typing
    jolod
    @jolod
    Btw, can't you use "scoped" type class instances in Haskell though?
    Jean-Louis Giordano
    @Jell
    do you mean like having a special type like with Sum & Product for Monoid?
    jolod
    @jolod
    I think Marco Zocca showed me that a lot time ago.
    No, not using newtypes.
    In PureScript type class instances are global, but I think this is not necessarily the case in Haskell, no?
    Jean-Louis Giordano
    @Jell
    I thought they were... yeah I think I meant the thing with newtype
    newtype Sum n = Sum n
    
    instance Num n => Semigroup (Sum n) where
      Sum x <> Sum y = Sum (x + y)
    
    instance Num n => Monoid (Sum n) where
      mempty = Sum 0
    
    newtype Product n = Product n
    
    instance Num n => Semigroup (Product n) where
      Product x <> Product y = Product (x * y)
    
    instance Num n => Monoid (Product n) where
      mempty = Product 1
    that's what I meant with Sum & Product
    "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?