I feel like although for nerds like me putting more types in a language is a cool thing, what would be much more important as a topic of research, in practise, is reducing the syntactic overhead of type systems. I recently heard so many complaints about this, I feel like we’re not there yet; I do agree. #haskell
I think what exhibits this problem is if you’re trying to rewrite a Python script in Haskell; sure, with Dynamic and a lot of rewriting you can get somewhere near the conciseness of the Python script but not when you’re actually trying to stay safe, even things like shelling out, bracketing resources and converting between string formats take up so much space that in most cases is just not justified at all. #haskell
@kosmikus the issue I see here is that for “trivial” things, the overhead is not justified; I’m not talking about the cases where types do actually help solving an issue (and I’m of the strong opinion, they do solve problems!).
To refer to the example again; think about writing Python in script-ish settings; most times you don’t need any types to oversee the situation, in these cases you probably don’t want to deal with their overhead, either; this starts by having to use fromIntegral, T.(un)pack, explicit lifting into monadic contexts, dealing with ambiguous types, and so on.
Another example is effect systems for that matter, every time you just “propagate” constraints, you end up with a flat record of effects that are mostly just syntactical noise, there’s no actual benefit in them, you’re just wrangling with the compiler. (Surely this is also a matter of design, think small functions with many effects and large functions with almost no effects, but this is something that exhibits in practice)
@mangoiv Oh, they're always enough. I think the main point in favour of generics-sop is that it leads to nicer and more high-level / composable code. The main point against is that it uses even more advaned type-level machinery and that it may incur and additional performance hit. I didn't take your statement as criticism. I just thought the argument "it adds more dependencies" against using it was a bit odd.
@kosmikus in what way? You have a lot more experience in such things so I’d be glad to know why you think this is bad/ makes you feel sadness? I saw that delroth also didn’t have much good to say…
@trebach@mangoiv@Janik To be fair, the "you'll just take what you're offered and you'll like it" role does exist in industry.
But I do not see why one would aspire to adopt the role of the badly treated intern. Nor do I view the surrounding context as particularly professional.
@bobkonf I tend to think that other people need these grants more urgently. I will probably come though, some crypto people gave me free money and i will use it for that 😌
Hey @kosmikus perhaps something you will like: https://mangoiv.com/ghci-module/ depending on what you said on the podcast. Still a bit barebones still but the idea is what you’re describing :3
@kosmikus@jaror I think I always underestimate the kind of overhead nix poses :/ I wouldn’t know how to make it easier from a user perspective though, give you a low power wrapper and a toml file? I guess this is a way to go?
I have written a little snippet in which I explore some "free" generic programming in Haskell, where you define your types as polynomials and then can use a lot of their structure to program on them, this enables more powerful things than deriving Foldable because the structure of the types actually enable the folding, not some compiler magic. I can already show that this works better by fmapping and folding types for free that we cannot (stock/ newtype) derive Foldable or Functor instances for in GHC. (thinking about newtype instances where the type variables don't occur in the correct spot)
I wrote a little snippet of what this can do (for example) at the very end. I would be happy about some feedback and especially whether this is novel enough to be worth a blogpost or something like that :)
@mangoiv Ah, I see. I think one disadvantage of this approach is that the generic representation is generally a more inefficient encoding than a "standard" Haskell datatype. So while you're now saving the effort of converting between representations, you're potentially making everything less efficient in turn.
But it might be interesting to try to measure this. I can't think of any Haskell generics approach that's currently advocating this, so it is somewhat novel, I think, but I may be lacking the complete picture.
The idea itself, I'd say, is perhaps the same that forms the basis of the Levitation papers (look for The Gentle Art of Levitation) as a starting point. That's not in a Haskell context, but it tries to envision a language where all datatypes are defined as being part of a generic universe, and the representations are the datatypes.
@kosmikus I have actually seen the levitation paper and I think I should give it a more thorough read again. Wrt. performance; I can imagine that this actually makes things worse but there are two thoughts that I had:
first of all, this might enable more chances to memoization because you might "accidentally" reuse programs
for the bigger picture: this is supposed to serve as a bit of a prototype of something I want to at some point implement as its own language (perhaps), and something else I want to do is "normalize" the types, s.t. isomorphic types are represented in the exact same way, meaning that after elaboration, there are less things to compile and there are more chances to memoization, this might also be useful in terms of how you program, I imagine that you write ++ like it is today on lists in Haskell and by that obtain + for Peano nats "for free" which might actually be worth the trouble?
Is it just me or is this whole thing about „don’t do X if you don’t really know what you’re doing“ really counter productive? Many people live in fear of X now and don’t start thinking if X is an actual problem or learn what the problems are that could rise from X.
I see this very often in the #haskell ecosystem where the solution to doing X properly is often learnt in a few minutes investigation.
@mangoiv I know I've said that a few times. Two examples I can think of:
AllowAmbiguousTypes, GHC suggests this but you should probably just use Proxy arguments instead.
Typeable, people coming from OOP languages often want a typeof function, but 99% of the time there is a better way to structure your programs using simple ADTs.
I still think these are not learnt in a few minutes. Even if that was the case, the most important thing you should learn is that you shouldn't use them very often.
@yvan I mean I still need a project for ZuriHac. So if you’re interested… Last year it didn’t work but perhaps now I have enough experiences @.@ afaiu we just need some c bindings and then just the rest sounds easy enough
@mangoiv Sure, abstracting from / parameterising over type classes is a good idea. I think Edsko did not want to use yet more features. He wasn't necessarily trying to say "write lots of types like SomeShowable". It was more like "if you're using any kind of existential, you might find yourself in a situation where you want quantified constraints".
FWIW, I think I'd probably go for an encoding where I just pair the existential with one constraint:
data Some :: Constraint -> (Type -> Type) -> Type where
Some :: c a => f a -> Some c f
And then use
class Top a
instance Top a
class (f a, g a) => And f g
instance (f a, g a) => And f g
(as e.g. defined in sop-core) to build the constraint I need.
Nesting your Has is neat, but not very usable without pattern synonyms.
@kosmikus yeah, perhaps my liking of pattern synonyms and type synonyms is a bit extreme :D
(also, of course, I didn't want to criticize Edsko but I wanted to add onto this, also because I couldn't really react to the youtube video because you need a google account >D)
It is a (somewhat wip) pastebin microblogging style written in Haskell using fused-effects, servant, one-time-password, lucid2, htmx, styled with bulma v1.
There’s a nixos module you can use to get it running on your machine.
@aka_dude i like it. I will perhaps rewrite in bluefin if I feel like it. Proper typed persistance abstraction would be first though, what I have now sucks.
random stuff:
I have long ago started writing Haskell types like: newtype A = MkA {unA :: B}, to avoid punning. So far, so good. However, someone told me that writing this: f (MkA b) = ... is somewhat odd because you don't MkA, you only do that the other way around. So I have started doing this very cursed thing everywhere I have a MkA-like constructor: f (unA -> b) = ...
Every time I see things like this, I feel very sad that people choose to be like this on the internet. I do use Hyprland but I will definitely keep steering clear of their surrounding community. This is really depressing.
@its_a_me@mdallastella the person in the screenshot repeatedly exhibited transphobia, I can attest of that. So it's much more like that vaxry person is cherry picking. This blogpost confirms to me he and his community is toxic. This is non-sense.