38 karma · joined April 14, 2023
This is possible to achieve (or hack your way through, if you will) by parameterizing the type and using a nullary type (a type which is impossible to have) to exclude specific cases of a sum type. In Haskell this would look like this:
data Weather a b c = Sunny a | Rainy b | Snowy c
-- can't snow in the summer!
onlySummerWeather :: forall a b. Weather a b Void -> String
onlySummerWeather weather = case weather of
Sunny _ -> "Got sunny weather"
Rainy _ -> "Got rainy weather"
Snowy v -> absurd v
That's an interesting idea. Do you have a link to show how you did this?
You're right, my memory has let me down.
> Do you have any pointers for the "load on tab" idea? I didn't turn up any good results in DDG and LLMs were just hallucinating.
The simplest implementation would be something like
bindkey ^I init_completions
init_completions () {
# ... init logic here ...
# rebind tab to complete
bindkey ^I complete-word
# actually do complete the initial request
zle complete-word
}
I'm curious where did you get that from.
Edit: I read the note in your dotfiles repo. Yes calling `compinit` on each shell invocation is going to be really slow. That's not how you're supposed to do it, you could at least add the `-C` flag to cache the completions. Ideally you'd also use `zcompile` to compile the cache to ZSH word code. This puts my completions initializing time at ~20ms on a lower/mid-end laptop. Additionally you can do the trick `fish` does and defer the initialization of completions until the first hit of Tab key, so the impact on shell startup time is exactly 0.
Programs can pollute it all they want, since I don't use it myself I also don't have to care about that.
splitString :: { pattern :: String, string :: String } -> Array String
splitString { pattern, string } = ...
splitString :: Pattern -> String -> Array String
splitString pattern string = ...Sorry, I must've been more explicit instead of implying certain usage patterns. What I meant here is that I have a hard time imagining this happening because I would start working on a function by writing its type signature. Unless my types check out, I won't be able to mark this function as "done" and jump to another part of code. So the situation "you return the partial assuming it's a number" simply can not happen, that's exactly what type checking is for. By the time I use it in another place, it has to already have been type checked.
So could you elaborate to me where the distinction lies here and why is there a need to "simulate" things?
I will get a type error and it will take me 2-3 seconds to figure out what it is about.
> Why on earth would you want to get a type error in a completely different part of the code because you got a function instead of an integer?
Why would it be in a completely different part of the code? At most it would be 2 lines away, but usually on the same line.
Maybe you could recall which learning materials you used?
[1] https://github.com/tree-sitter/tree-sitter/issues/130#issuec...
If this wasn't the case, how would the information about what you got be retained? It's either positional, or by a tag/key (row-polymorphic variants), or none retained.
I don't see why would you want to use monadic API for approaching an "anonymous sum type" problem in the first place. As I said before, there are fundamentally just 2 operations you would want to use: inject and project. Maybe you could also mention assoc for re-association but I'd say if you're using it you're likely handling the problem the wrong way. So I still don't see how monad transformers play into this. They are a nice (decent, at least) trick for dealing with some situations but the problem we're talking about here isn't one of them.
> so we'd want all nested variations normalized to Either<A,B>.
Sorry, perhaps my thinking is shaped by nominal type systems rather than structural, but if the only thing we care about is whether the type is A, then how do we end up having Either<Either<A, B>, A>> in the first place? Thinking about this in terms of a nominal type system, the specific type you present here has to have some specific meaning associated with, specifically, this type, otherwise we would have chosen some other type. So the key thing here is that if we have Either<A, A> then it HAS to be distinct from simply A, otherwise we wouldn't have this type in the first place. Us constructing it means we associate it with a specific meaning so it has to be distinct from A. But if we DON'T care, then, I guess, we shouldn't use this type? Use the type we do care about? The same goes for Either<A, B> and Either<B, A>.
> or we need to hide the complexity by using more abstract tools like e.g. monad transformers
This is interesting, how do monad transformers relate to this problem?
We didn't start with composability as a requirement but you're right in that if it's a goal then nesting Either's is a rather poor solution. A better fit would be variants based on row polymorphism as I described in the reply to the other poster.
It wouldn't be a 1:1 mapping to your first example though, if your union is ultimately closed (as in your first example) then you'd still need to have one extra no-op function call to unify the types. Not a big deal but row-polymorphic variants lose here. On the other hand, IMO the possibility of having them open as well is the killer feature.
Ultimately though, I don't like this style of type unification as the one happening in your first example. Shaped by the languages I'm working with, I simply don't end up in situations where I'd need something like this. I just approach the problems differently. But this is more of a subjective territory here.
This is understandable. But what does it have to do with "collapsing" `a | a` into `a`? Throughout your post I think you're talking about plain untagged union types but that's something the guy I've been replying to already ruled out. Position problem can be handled beautifully by variants based on row polymorphism, such as in OCaml or PureScript. There you can access the fields not by their position but by a key, like keys in objects in JS, meaning that they don't have to be ordered at all. It's like an inverse of a struct: in a struct all fields/keys are guaranteed to exist, but in a variant only one of them exists. Due to row polymorphism they can also be extensible. You can even "handle" a particular field/key and remove it from the type but keep all the other ones and delay handling them.
> you also might not care whether it's an (encoding as) Either<A,B> or SomeoneElsesEither<A,B>
This is a theoretical issue but in practice I don't think I've ever seen anyone using some non-standard Either-like datatype in languages I've dealt with. Where Either needs to be used people just use Either.
> and you also don't want to have to deal with flattening nested Either's as in the example
What would "flattening" mean here? Fundamentally there are only 2 operations you can do on a generic sum type like this: either inject a value (construct the type) or try to get the value at a certain position. You might also think pattern matching will get tedious, but that's not the case either, you can just have a function `actOnAorBorC` and call it with `actOnA`, `actOnB` and `actOnC` and do the pattern matching inside these functions.
Why would you want the former to type check as the latter? Where do you see the complexity?
But you just said "For example `A | B | A` is the same type as `A | B`". How would this be possible for tagged union types?
> that does not require naming a new type to use
> This is also not covered by the Either/Result type
It's more probable that I'm just not understanding what you're talking about, but *the only* re-usable tagged union type similar to tuples is *the* sum type.
Let's say you're dealing coffee. People want it either with sugar or without sugar. You don't want to create a new sum type CoffeeFlavor? Fine, just use Either<Sugar, NoSugar>. This is *the* equivalent of a tuple. You need more than 2 options? No problem, Either<Sugar, Either<JustABit, NoSugar>>. I don't know what else could be a "anonymous tagged union".
> This is useful as a shorthand when you don't want/need a new type to represent your problem, similar to tuples.
Yes this is handled perfectly by the generic sum type, you don't need untagged unions for this. Rust used to have Either in its standard library, but they removed it and kept Result only. Semantically they're the same (a ⊕ b) but Result's name implies it has something to do with some "results". Anyways nothing stops you from creating one yourself, or even using Result if you're fine with the weird-sounding name.
But this is just a generic sum type?
data Sum a b = L a | R b
infixr 5 type Sum as ⊕
type E₂ a b z = a ⊕ b ⊕ z
type E₃ a b c z = a ⊕ b ⊕ c ⊕ z
-- and so on…
type E₃AndNoMore a b c = a ⊕ b ⊕ c ⊕ Void
fact n = do
let n' = n - 1
if n <= 1 then 1 else n * fact n'
I think the article implies it clear enough that it's impossible. Even if your monad has nonsensical (but lawful) semantics like `Proxy t` it's still possible to use it with `strength`. BTW the `strength` function is called `sequence`.