monochrom 2017-02-01 08:48:21
My favourite proof technique is to reduce the statement-to-be-proved to a vacuously true statement. This is called proof nihilism.
ertes 2017-02-01 08:49:08
is there a base library way of constructing a global IORef (or something similar) that will survive a GHCi reload?
c_wraith 2017-02-01 08:50:03
I'm not sure that even is a coherent thing to ask for.
c_wraith 2017-02-01 08:50:24
what if you're storing a value of some type that is changed in the reload?
c_wraith 2017-02-01 08:50:49
seems nicely equivalent to unsafeCoerce
ertes 2017-02-01 08:52:22
oh, Data.Unique already survives reloads
ski 2017-02-01 08:52:24
the interactor could possibly distinguish between the old and the new version of the type, at least assuming the definition changed
hexagoxel 2017-02-01 08:53:01
ertes: you are aware of Rapid? (not sure if relevant, but seems atleast somewhat related)
ertes 2017-02-01 08:53:11
hexagoxel: i'm the author of rapid =)
hexagoxel 2017-02-01 08:53:40
well, glad i could help. :p
c_wraith 2017-02-01 08:53:44
but are you aware of it? sometimes I forget things I've done!
edwardk 2017-02-01 08:54:08
monochrome: the first real experience i had with that was the dyad paper https://maartenfokkinga.github.io/utwente/mmf94c.pdf which has a ridiculously strongnatural isomorphism requirement in the middle which prevents any interesting ones from existing
ski 2017-02-01 08:54:30
(e.g. in the SML/NJ interactor, a new definition of a data type `foo' will shadow the old one. values whose types involve the old `foo' will still be usable, but the old `foo' (iirc then prefixed with a `?.') is considered different from the new one)
ertes 2017-02-01 08:54:35
rapid uses foreign-store to achieve that though, which i hope to avoid… and Data.Unique isn't specific enough (it doesn't guarantee that the values are sequential, so in principle they could collide early by virtue of the birthday paradox)
ertes 2017-02-01 08:54:48
(i only need unique Int identifiers)
monochrom 2017-02-01 08:55:01
wait, Fokkinga has a github too?!
edwardk 2017-02-01 08:55:30
found it while looking for a copy of the paper to complain about ;)
c_wraith 2017-02-01 08:56:19
edwardk, does it more or less restrict you to things equivalent to Identity?
edwardk 2017-02-01 08:56:21
looks like he logged in for a couple of days in 2014 and never touched it again
monochrom 2017-02-01 08:56:35
haha
edwardk 2017-02-01 08:56:37
c_wraith: it restricts you to things where one or the other of the monad or comonad are identity
c_wraith 2017-02-01 08:56:47
ah
edwardk 2017-02-01 08:57:14
i fiddled with it back when i started category-extras
monochrom 2017-02-01 08:58:36
How does Data.Unique manage to survive reloads?
dolio 2017-02-01 08:59:16
Does it?
c_wraith 2017-02-01 08:59:34
I think it does because usually packages aren't reloaded.
monochrom 2017-02-01 08:59:45
Ah!
c_wraith 2017-02-01 08:59:47
only interpreted code is reloaded, usually.
dmwit 2017-02-01 09:01:53
ertes: Perhaps the usual unsafePerformIO/NOINLINE tricks would work if applied to an `IO (IORef a)` which read from a file to choose the initial value and used an API that wrote to the file on each write to the ref.
ski 2017-02-01 09:02:05
edwardk : regarding a discussion on #haskell-beginners (with adamCS) three weeks ago involving `(:-)' from `constraints' -- have you tried implementing a mapping operation over an existential-thing-with-constraint, of type `forall c d f g. (forall a. c a :- d a) -> (forall a. f a -> g a) -> (exists a. c a *> f a) -> (exists a. d a *> g a)' ?
edwardk 2017-02-01 09:02:55
oh just a bifunctor like thing?
edwardk 2017-02-01 09:03:21
in something like hask that'd be easy
ski 2017-02-01 09:03:22
edwardk : yes, but `c,f :: * -> Constraint'
ski 2017-02-01 09:03:31
er, `c,d :: ...'
lyxia 2017-02-01 09:03:42
constraints doesn't seem beginner friendly.
dmwit 2017-02-01 09:04:11
Depends on the beginner.
lyxia 2017-02-01 09:04:13
What's *>
dmwit 2017-02-01 09:04:43
`c *> a` is like `(Dict c, a)`
edwardk 2017-02-01 09:04:44
(forall a. c a :- d a) would involve using Nat (:~:) (:-), while (forall a. f a -> g a) inhask would involve using Nat (:~:) (->)
ski 2017-02-01 09:05:23
edwardk : i noticed it seemed to be tricker to get GHC to accept it, than initially expected -- involving needing to define a local helper with an explicit type signature, in order to force it to use the particular hidden `a' with `c a :- d a'
edwardk 2017-02-01 09:05:42
but it doesn't have anything for doing (exists a. c a *> f a) that is a bit of a mess
dmwit 2017-02-01 09:05:43
lyxia: (ski invented this notation, it doesn't exist in any Haskell implementation or library as far as I know)
ski 2017-02-01 09:06:04
lyxia : to use a value of type `c => a', you must first provide evidence for the constraint `a', then you can use it as a value of type `a'
ski 2017-02-01 09:06:28
lyxia : a value of type `c *> a' otoh carries with it evidence for `c', together with a value of type `a'
ski 2017-02-01 09:07:36
`(*>)' is to `(=>)' what `(,)' is to `(->)'
lyxia 2017-02-01 09:08:01
Oh I see. Thanks.
lyxia 2017-02-01 09:08:40
constraints has Nat and Symbol modules now! lots of fun!
ski 2017-02-01 09:08:47
(the old discussion in questions starts at )
monochrom 2017-02-01 09:09:50
Oh God, it is going to do type-level gcd too?
monochrom 2017-02-01 09:10:27
Sounds like the C++ joke about prime factorization at compile time (so O(1) run time) is becoming true for Haskell.
dolio 2017-02-01 09:11:44
I don't think that's r ight.
ski 2017-02-01 09:12:19
i suppose it's doing a `reflection' trick ?
dolio 2017-02-01 09:12:33
o shouldn't be universal.
lyxia 2017-02-01 09:12:48
magic is an unsafe internal function
dolio 2017-02-01 09:12:58
Oh.
ski 2017-02-01 09:15:57
i suppose you'd be happier with `lessMagic :: (Integer -> Integer -> Integer) -> (forall n m. (KnownNat n,KnownNat m) :- exists o. KnownNat o)' or `lessMagic :: (Integer -> Integer -> Integer) -> exists f. (forall n m. (KnownNat n,KnownNat m) :- KnownNat (f n m))' (in the former case assuming an `exists' that works for constraints) ?
ski 2017-02-01 09:17:01
(and then an `unsafeCoerce' to turn the unknown result constraint into the particular constraint desired, here `Gcd n m')
Zemyla 2017-02-01 09:23:27
I wonder if there's a good way to do random number generators as linear types.
ski 2017-02-01 09:23:35
edwardk : where's `(:~:)' ?
monochrom 2017-02-01 09:24:35
Yes but first you need linear types or uniqueness types.
c_wraith 2017-02-01 09:24:39
affine?
ski 2017-02-01 09:24:57
affine would probably work here as well ..
dolio 2017-02-01 09:25:15
Uniqueness is not what you want, I think.
c_wraith 2017-02-01 09:25:31
in that case, just go do it in rust. it gives you affine types. :)
dolio 2017-02-01 09:25:37
I guess it depends what you want, really.
dolio 2017-02-01 09:26:05
But uniqueness lets you know if you're allowed to mutate something because you haven't made multiple references to it.
dolio 2017-02-01 09:26:26
Whereas for a random generator, you might care about not ever being able to reference it twice.
dolio 2017-02-01 09:26:58
Not merely being at liberty to modify it in place.
ertes 2017-02-01 09:27:14
dmwit: too much engineering… this is for *sortable* references to haskell values
ertes 2017-02-01 09:28:25
i'm considering StableName, but then there is no uniqueness guarantee, so i need to use HashMap
ertes 2017-02-01 09:30:29
this should be a lot easier than it is =/
ertes 2017-02-01 09:32:21
it would be nice if Data.Unique would specify explicitly that the generated values are sequential
ertes 2017-02-01 09:33:15
or rather than hashUnique will only collide after the whole range of Int has been exhausted
ertes 2017-02-01 09:33:57
s/than/that/
edwardk 2017-02-01 09:35:08
ski: Data.Type.Equality or whatever
ski 2017-02-01 09:35:27
ok
edwardk 2017-02-01 09:36:05
serves as a usable form of the discrete category of hask or pretty much anything else where every type in the kind is an object of the category
