Newest at the top
2025-09-08 22:13:16 +0200 | <tomsmeding> | is it? |
2025-09-08 22:13:10 +0200 | <ski> | from `\(Just x) -> \(Just y) -> ..x..y..' .. |
2025-09-08 22:13:07 +0200 | chele_ | (~chele@user/chele) (Ping timeout: 255 seconds) |
2025-09-08 22:12:59 +0200 | <ski> | er |
2025-09-08 22:12:55 +0200 | <ski> | there's also the issue that `\(Just x) (Just y) -> ..x..y..' is distinct from `\(Just x) -> (Just y) -> ..x..y..' .. |
2025-09-08 22:12:48 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
2025-09-08 22:12:22 +0200 | <tomsmeding> | meh |
2025-09-08 22:12:20 +0200 | <tomsmeding> | \ @a (Eq a) => \ @b (Ord b) => \..a..b.. -> ..a..b.. |
2025-09-08 22:12:09 +0200 | <ski> | yea, was just thinking about curlies |
2025-09-08 22:11:55 +0200 | <ski> | \ @a (Eq a) => \..a.. -> ..a.. -- hmm |
2025-09-08 22:11:50 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-09-08 22:11:40 +0200 | <tomsmeding> | except that {} is taken for records |
2025-09-08 22:11:31 +0200 | <tomsmeding> | perhaps `\ @a {Eq a} ..a.. -> ..a..' would make more sense, to syntactically distinguish it from a normal argument |
2025-09-08 22:11:00 +0200 | <tomsmeding> | which, well, is not haskell-y :p |
2025-09-08 22:10:52 +0200 | <tomsmeding> | `\ @a (Eq a) ..a.. -> ..a..' |
2025-09-08 22:10:46 +0200 | <ski> | yes |
2025-09-08 22:10:39 +0200 | <tomsmeding> | if you're going System-F-style, it would be a separate argument |
2025-09-08 22:10:36 +0200 | <ski> | (without needing to put in a separate signature, or an ascription on the whole thing) |
2025-09-08 22:10:11 +0200 | <ski> | the other thing i was pondering, when i wanted `\ @a ..a.. -> ..a..', was how to specify constraints here |
2025-09-08 22:10:07 +0200 | chele__ | (~chele@user/chele) chele |
2025-09-08 22:09:47 +0200 | <tomsmeding> | having types next to the arguments instead of in a disconnected list is helpful |
2025-09-08 22:09:33 +0200 | <tomsmeding> | being able to forgo a type signature if you fully specify types of the patterns and the RHS would make lots of people happy |
2025-09-08 22:09:01 +0200 | <tomsmeding> | right |
2025-09-08 22:08:43 +0200 | <tomsmeding> | "I needed to give just this little bit of extra info for the compiler to typecheck my code, but I'm not going to give you the luxury of just seeing the resulting inferred type in one place!" |
2025-09-08 22:08:16 +0200 | <ski> | i'd like to have the option to have either a separate type signature, or ascriptions on the parameter patterns and the definiendum |
2025-09-08 22:07:46 +0200 | <tomsmeding> | I agree that that would be a sensible extension to PartialTypeSignatures, but I wouldn't use it |
2025-09-08 22:07:22 +0200 | <tomsmeding> | I like my type signatures :p |
2025-09-08 22:07:17 +0200 | <ski> | yep, this would act as an enhancement, to that |
2025-09-08 22:06:56 +0200 | <tomsmeding> | oh, PartialTypeSignatures++? |
2025-09-08 22:06:34 +0200 | <ski> | foo x y = ... |
2025-09-08 22:06:29 +0200 | <ski> | foo :: _a -> _a -> ... |
2025-09-08 22:06:29 +0200 | <tomsmeding> | yeah forall with ScopedTypeVariables is bonkers |
2025-09-08 22:06:18 +0200 | <tomsmeding> | but IMO, if you care about the details of what type variables get generalised and which don't, it's much better for readability if you write out the type signature anyway |
2025-09-08 22:05:58 +0200 | <ski> | yea, `forall' behaves the opposite of what i would expect, with `ScopedTypeVariables' |
2025-09-08 22:05:43 +0200 | <tomsmeding> | right, it's when you explicitly skip part (or all) of a type signature that this becomes relevant |
2025-09-08 22:05:34 +0200 | <ski> | where you don't want to specify some part of the signature, letting be inferred. but specifying that one part needs to be the same as another part |
2025-09-08 22:05:22 +0200 | <tomsmeding> | because ScopedTypeVariables' `forall`-based syntax is iffy |
2025-09-08 22:05:07 +0200 | <ski> | `_a' would kinda be useful for partial type signatures |
2025-09-08 22:05:05 +0200 | <tomsmeding> | the only reason I write type signatures or type applications in patterns in haskell is to bind type variables to be used in the body, really |
2025-09-08 22:04:32 +0200 | Googulator | (~Googulato@2a01-036d-0106-28ad-1d1d-edbe-776a-384c.pool6.digikabel.hu) |
2025-09-08 22:04:14 +0200 | Googulator | (~Googulato@2a01-036d-0106-28ad-1d1d-edbe-776a-384c.pool6.digikabel.hu) (Quit: Client closed) |
2025-09-08 22:04:14 +0200 | <tomsmeding> | sure |
2025-09-08 22:04:08 +0200 | <tomsmeding> | but I'm not sure that distinction would be helpful in practice in writing haskell code |
2025-09-08 22:04:07 +0200 | <ski> | `a' wouldn't need to be bound at `foo', though. could be bound by some surrounding context |
2025-09-08 22:03:38 +0200 | <tomsmeding> | that distinction makes sense to me |
2025-09-08 22:03:32 +0200 | <ski> | yes |
2025-09-08 22:03:31 +0200 | <tomsmeding> | right |
2025-09-08 22:03:26 +0200 | <ski> | or, would also work without the type signature |
2025-09-08 22:03:18 +0200 | <tomsmeding> | in contrast to, in your idealised syntax, `foo (n :: a) = ...` which would require that `a` is a skolem |
2025-09-08 22:03:14 +0200 | <ski> | yes |