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 +0200 | chele_ | (~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 +0200 | merijn | (~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 +0200 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Client Quit) |
2025-09-08 21:55:07 +0200 | humasect | (~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 +0200 | peterbecich | (~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 +0200 | merijn | (~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 +0200 | davidlbowman | (~dlb@user/davidlbowman) davidlbowman |
2025-09-08 21:42:07 +0200 | target_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 |