2025/09/08

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 +0200chele_(~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 +0200tzh(~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 +0200merijn(~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 +0200chele__(~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 +0200Googulator(~Googulato@2a01-036d-0106-28ad-1d1d-edbe-776a-384c.pool6.digikabel.hu)
2025-09-08 22:04:14 +0200Googulator(~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