Logs: liberachat/#haskell
| 2025-09-08 19:28:27 | → | trickard_ joins (~trickard@cpe-53-98-47-163.wireline.com.au) |
| 2025-09-08 19:32:57 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds) |
| 2025-09-08 19:40:10 | × | davidlbowman quits (~dlb@user/davidlbowman) (Ping timeout: 258 seconds) |
| 2025-09-08 19:40:15 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-08 19:40:18 | × | trickard_ quits (~trickard@cpe-53-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-09-08 19:40:32 | → | trickard_ joins (~trickard@cpe-53-98-47-163.wireline.com.au) |
| 2025-09-08 19:41:00 | <ski> | "if you supply a type signature, you can already do something like the second" -- i tried this, recently, didn't look good in that case |
| 2025-09-08 19:41:28 | <ski> | oh, and i don't necessarily want plain `PatternSignatures' to bind tyvars, really |
| 2025-09-08 19:42:01 | <ski> | (the `\ @a ..a.. -> ..a..' obviously would, though) |
| 2025-09-08 19:42:07 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 2025-09-08 19:42:12 | → | davidlbowman joins (~dlb@user/davidlbowman) |
| 2025-09-08 19:44:41 | <ski> | % let foo :: Int -> Bool; foo (n :: a) = n == (0 :: a) in foo 42 |
| 2025-09-08 19:44:41 | <yahb2> | False |
| 2025-09-08 19:45:14 | <ski> | this is kinda confusing. istr something similar being discussed in some ML |
| 2025-09-08 19:45:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-09-08 19:45:45 | <geekosaur> | looks like pre-6.4 scoped tyvars |
| 2025-09-08 19:46:09 | <ski> | mm |
| 2025-09-08 19:46:55 | <ski> | hm |
| 2025-09-08 19:46:57 | <ski> | fun foo (m : int) (n : 'a) = m <> n; |
| 2025-09-08 19:46:59 | <tomsmeding> | I also think binding type variables via a type annotation in a pattern is a bit odd, but that's what the extension does now |
| 2025-09-08 19:47:03 | <ski> | in SML gives type error |
| 2025-09-08 19:47:27 | <tomsmeding> | and, to be honest, it's useful sometimes |
| 2025-09-08 19:47:59 | <tomsmeding> | (though typically one would be able to get away with a type application to a constructor pattern) |
| 2025-09-08 19:48:40 | × | peterbecich quits (~Thunderbi@syn-172-222-149-049.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2025-09-08 19:48:57 | <tomsmeding> | % foo (Just @a x) = x :: a -- ski: do you also think this is bad? |
| 2025-09-08 19:48:57 | <yahb2> | <no output> |
| 2025-09-08 19:50:18 | <ski> | fun ('a,'b) map f [] = [] | map f (x::xs) = f x :: map f xs; |
| 2025-09-08 19:50:21 | <ski> | works |
| 2025-09-08 19:51:03 | <ski> | tomsmeding : yea, that would be my preferred way, for existentials |
| 2025-09-08 19:52:07 | <ski> | tomsmeding : no, since `a' there is skolem |
| 2025-09-08 19:52:55 | <ski> | hm |
| 2025-09-08 19:52:57 | <ski> | let foo (m : int) (n : 'a) = m <> n;; |
| 2025-09-08 19:53:03 | <haskellbridge> | <magic_rb> tomsmeding still don't have my irc bridge, but quickie question. Are you at all familiar with implementing the STG? I want to try to implement a nix evaluator using an STG |
| 2025-09-08 19:53:16 | <ski> | in OCaml (similarly confusingly) works |
| 2025-09-08 19:53:24 | <ski> | that's probably the one i was thinking of |
| 2025-09-08 19:53:26 | <tomsmeding> | ski: to me, `foo (Just @a x) = x :: a` and `foo (Just x :: Maybe a) = x :: a` feel about the same in terms of "weird scoping" |
| 2025-09-08 19:53:49 | <tomsmeding> | with `foo @a (Just x) = x :: a` being materially different |
| 2025-09-08 19:54:13 | <ski> | tomsmeding : i agree |
| 2025-09-08 19:54:20 | <tomsmeding> | magic_rb: I have 0.0001 idea of how STG works |
| 2025-09-08 19:54:35 | <tomsmeding> | magic_rb: check this https://github.com/quchen/stgi |
| 2025-09-08 19:54:46 | <ski> | but what i was on about was having a type variable that didn't stand for a skolem, there, but some specific type |
| 2025-09-08 19:55:01 | <tomsmeding> | not sure how up to date it is with the latest version of STG in GHC, but when I found it long ago I thought it was a neat way to at least illustrate the ideas |
| 2025-09-08 19:55:07 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2025-09-08 19:55:08 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Client Quit) |
| 2025-09-08 19:55:41 | <tomsmeding> | ski: right, my first two examples work just fine with ghc even if `foo :: Maybe Int -> Int` |
| 2025-09-08 19:55:58 | <ski> | right |
| 2025-09-08 19:56:06 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-09-08 19:56:10 | <tomsmeding> | is that what you mean? |
| 2025-09-08 19:56:10 | <haskellbridge> | <magic_rb> tomsmeding im reading the original paper and its very readable. But ill try stgi once I actually start putting down rust code |
| 2025-09-08 19:56:15 | <ski> | i wouldn't object to it, if `_a' was used instead of `a' |
| 2025-09-08 19:56:54 | <tomsmeding> | is that like Agda's `.a' syntax, a pattern that doesn't match but is fully determined by other patterns? |
| 2025-09-08 19:57:17 | <ski> | idea being that `_a' is an arbitrary meta-variable (/ logic variable / dataflow variable), which can stand for some specific type |
| 2025-09-08 19:57:24 | <ski> | no |
| 2025-09-08 19:57:36 | → | chele_ joins (~chele@user/chele) |
| 2025-09-08 19:58:01 | <tomsmeding> | but would you then not also want the syntax to really be `foo (Just @_a _x) = x :: a`? |
| 2025-09-08 19:58:14 | <tomsmeding> | because that _x is also a pattern variable that stands for some specific value |
| 2025-09-08 19:58:42 | <ski> | if you type `id :: forall a. a -> a; id x = x' (not having `ScopedTypeVariables' in mind here, really), then `a' here (type of `x') is a skolem, can't be unified with any other type |
| 2025-09-08 19:59:27 | <ski> | if you instead type `id x = x' (no explicit signature), then type inferred for `id' is `_a -> _a', which is then *generalized* to `forall a. a -> a' |
| 2025-09-08 20:00:22 | <ski> | in the MLs, in some cases, the generalization part does not happen. then, the `_a' might get instantiated later, refining the type signature, fixing `_a' to something more specific |
| 2025-09-08 20:00:27 | <tomsmeding> | ski: ah you're specifically thinking about the case where there is no type signature? |
| 2025-09-08 20:00:42 | × | chele quits (~chele@user/chele) (Ping timeout: 252 seconds) |
| 2025-09-08 20:00:52 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-09-08 20:01:03 | <ski> | (SML/NJ simply replaces it with an unknown abstract data type, `?.X1',&c. in unknown module `?', doesn't allow later refinement in this way) |
| 2025-09-08 20:01:16 | <ski> | i'm talking about both, tomsmeding |
| 2025-09-08 20:01:27 | <tomsmeding> | right |
| 2025-09-08 20:01:55 | <ski> | but explaining what i mean by `_a' here, why i think it'd be okay for `foo :: Int -> Bool; foo (n :: _a) = n == (0 :: _a)' |
| 2025-09-08 20:02:24 | <tomsmeding> | oh I see |
| 2025-09-08 20:02:29 | <ski> | because it's a clear hint that `_a' may not be abstract/opaque/forgotten/hidden/skolem |
| 2025-09-08 20:02:48 | <tomsmeding> | that _a is a unification variable that then gets unified with Int when the type signature is applied |
| 2025-09-08 20:02:53 | × | polykernel quits (~polykerne@user/polykernel) (Remote host closed the connection) |
| 2025-09-08 20:03:14 | <ski> | yes |
| 2025-09-08 20:03:18 | <tomsmeding> | in contrast to, in your idealised syntax, `foo (n :: a) = ...` which would require that `a` is a skolem |
| 2025-09-08 20:03:26 | <ski> | or, would also work without the type signature |
| 2025-09-08 20:03:31 | <tomsmeding> | right |
| 2025-09-08 20:03:32 | <ski> | yes |
| 2025-09-08 20:03:38 | <tomsmeding> | that distinction makes sense to me |
| 2025-09-08 20:04:07 | <ski> | `a' wouldn't need to be bound at `foo', though. could be bound by some surrounding context |
| 2025-09-08 20:04:08 | <tomsmeding> | but I'm not sure that distinction would be helpful in practice in writing haskell code |
| 2025-09-08 20:04:14 | <tomsmeding> | sure |
| 2025-09-08 20:04:14 | × | Googulator quits (~Googulato@2a01-036d-0106-28ad-1d1d-edbe-776a-384c.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-09-08 20:04:32 | → | Googulator joins (~Googulato@2a01-036d-0106-28ad-1d1d-edbe-776a-384c.pool6.digikabel.hu) |
| 2025-09-08 20:05:05 | <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 20:05:07 | <ski> | `_a' would kinda be useful for partial type signatures |
| 2025-09-08 20:05:22 | <tomsmeding> | because ScopedTypeVariables' `forall`-based syntax is iffy |
| 2025-09-08 20:05:34 | <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 20:05:43 | <tomsmeding> | right, it's when you explicitly skip part (or all) of a type signature that this becomes relevant |
| 2025-09-08 20:05:58 | <ski> | yea, `forall' behaves the opposite of what i would expect, with `ScopedTypeVariables' |
| 2025-09-08 20:06:18 | <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 20:06:29 | <tomsmeding> | yeah forall with ScopedTypeVariables is bonkers |
| 2025-09-08 20:06:29 | <ski> | foo :: _a -> _a -> ... |
| 2025-09-08 20:06:34 | <ski> | foo x y = ... |
| 2025-09-08 20:06:56 | <tomsmeding> | oh, PartialTypeSignatures++? |
| 2025-09-08 20:07:17 | <ski> | yep, this would act as an enhancement, to that |
| 2025-09-08 20:07:22 | <tomsmeding> | I like my type signatures :p |
| 2025-09-08 20:07:46 | <tomsmeding> | I agree that that would be a sensible extension to PartialTypeSignatures, but I wouldn't use it |
| 2025-09-08 20:08:16 | <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 20:08:43 | <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 20:09:01 | <tomsmeding> | right |
| 2025-09-08 20:09:33 | <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 20:09:47 | <tomsmeding> | having types next to the arguments instead of in a disconnected list is helpful |
All times are in UTC.