2025/09/08

Newest at the top

2025-09-08 21:58:42 +0200 <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 21:58:14 +0200 <tomsmeding> because that _x is also a pattern variable that stands for some specific value
2025-09-08 21:58:01 +0200 <tomsmeding> but would you then not also want the syntax to really be `foo (Just @_a _x) = x :: a`?
2025-09-08 21:57:36 +0200chele_(~chele@user/chele) chele
2025-09-08 21:57:24 +0200 <ski> no
2025-09-08 21:57:17 +0200 <ski> idea being that `_a' is an arbitrary meta-variable (/ logic variable / dataflow variable), which can stand for some specific type
2025-09-08 21:56:54 +0200 <tomsmeding> is that like Agda's `.a' syntax, a pattern that doesn't match but is fully determined by other patterns?
2025-09-08 21:56:15 +0200 <ski> i wouldn't object to it, if `_a' was used instead of `a'
2025-09-08 21:56:10 +0200 <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 21:56:10 +0200 <tomsmeding> is that what you mean?
2025-09-08 21:56:06 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-09-08 21:55:58 +0200 <ski> right
2025-09-08 21:55:41 +0200 <tomsmeding> ski: right, my first two examples work just fine with ghc even if `foo :: Maybe Int -> Int`
2025-09-08 21:55:08 +0200humasect(~humasect@dyn-192-249-132-90.nexicom.net) (Client Quit)
2025-09-08 21:55:07 +0200humasect(~humasect@dyn-192-249-132-90.nexicom.net)
2025-09-08 21:55:01 +0200 <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 21:54:46 +0200 <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 21:54:35 +0200 <tomsmeding> magic_rb: check this https://github.com/quchen/stgi
2025-09-08 21:54:20 +0200 <tomsmeding> magic_rb: I have 0.0001 idea of how STG works
2025-09-08 21:54:13 +0200 <ski> tomsmeding : i agree
2025-09-08 21:53:49 +0200 <tomsmeding> with `foo @a (Just x) = x :: a` being materially different
2025-09-08 21:53:26 +0200 <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 21:53:24 +0200 <ski> that's probably the one i was thinking of
2025-09-08 21:53:16 +0200 <ski> in OCaml (similarly confusingly) works
2025-09-08 21:53:03 +0200 <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 21:52:57 +0200 <ski> let foo (m : int) (n : 'a) = m <> n;;
2025-09-08 21:52:55 +0200 <ski> hm
2025-09-08 21:52:07 +0200 <ski> tomsmeding : no, since `a' there is skolem
2025-09-08 21:51:03 +0200 <ski> tomsmeding : yea, that would be my preferred way, for existentials
2025-09-08 21:50:21 +0200 <ski> works
2025-09-08 21:50:18 +0200 <ski> fun ('a,'b) map f [] = [] | map f (x::xs) = f x :: map f xs;
2025-09-08 21:48:57 +0200 <yahb2> <no output>
2025-09-08 21:48:57 +0200 <tomsmeding> % foo (Just @a x) = x :: a -- ski: do you also think this is bad?
2025-09-08 21:48:40 +0200peterbecich(~Thunderbi@syn-172-222-149-049.res.spectrum.com) (Ping timeout: 248 seconds)
2025-09-08 21:47:59 +0200 <tomsmeding> (though typically one would be able to get away with a type application to a constructor pattern)
2025-09-08 21:47:27 +0200 <tomsmeding> and, to be honest, it's useful sometimes
2025-09-08 21:47:03 +0200 <ski> in SML gives type error
2025-09-08 21:46:59 +0200 <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 21:46:57 +0200 <ski> fun foo (m : int) (n : 'a) = m <> n;
2025-09-08 21:46:55 +0200 <ski> hm
2025-09-08 21:46:09 +0200 <ski> mm
2025-09-08 21:45:45 +0200 <geekosaur> looks like pre-6.4 scoped tyvars
2025-09-08 21:45:24 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-09-08 21:45:14 +0200 <ski> this is kinda confusing. istr something similar being discussed in some ML
2025-09-08 21:44:41 +0200 <yahb2> False
2025-09-08 21:44:41 +0200 <ski> % let foo :: Int -> Bool; foo (n :: a) = n == (0 :: a) in foo 42
2025-09-08 21:42:12 +0200davidlbowman(~dlb@user/davidlbowman) davidlbowman
2025-09-08 21:42:07 +0200target_i(~target_i@user/target-i/x-6023099) target_i
2025-09-08 21:42:01 +0200 <ski> (the `\ @a ..a.. -> ..a..' obviously would, though)
2025-09-08 21:41:28 +0200 <ski> oh, and i don't necessarily want plain `PatternSignatures' to bind tyvars, really