beaky 2017-02-28 10:45:20
byorgey: so i can verify my BST is ordered everywhere
mniip 2017-02-28 10:45:39
Rupsbant_, I suppose it may, but only in optimized code
byorgey 2017-02-28 10:45:40
beaky: just because you have an Ord constraint does not actually mean it satisfies the BST invariant
beaky 2017-02-28 10:45:44
ah
byorgey 2017-02-28 10:46:01
it just means elements of the type can be compared
beaky 2017-02-28 10:46:20
hmm this is better but it seems to not like the `mappend`? https://ideone.com/hgUxxG
nshepperd_ 2017-02-28 10:46:43
dmwit: plus, probably want to make it a strict structure
beaky 2017-02-28 10:47:07
byorgey hmm so how do i make sure it is always bst invariant
Rupsbant_ 2017-02-28 10:47:45
mniip but its not really known? Then ill have to test this myself. Thanks
dmwit 2017-02-28 10:48:10
beaky: If you want the compiler to check this for you, you are probably going to prefer working in a language with more proof capabilities than GHC has.
byorgey 2017-02-28 10:48:14
beaky: your choices are (1) prove it yourself, or (2) write the code in Agda/Coq/Idris/etc. and encode the BST invariant in the types.
mbw 2017-02-28 10:48:15
I was thinking about mentioning that, but I have no idea if people use bang patterns and unpack pragmas by default.
beaky 2017-02-28 10:48:21
ah
beaky 2017-02-28 10:48:29
hmm ok i will check those out
dmwit 2017-02-28 10:48:44
You might look at Liquid Haskell (don't know if it has the necessary power), or one of the dependently typed languages floating around like Agda, Coq, or Idris.
dmwit 2017-02-28 10:49:27
beaky: Practically, the most popular solution is to write the code carefully, following a known and proven-on-paper algorithm, and test it a lot. =)
mniip 2017-02-28 10:49:34
Rupsbant_, that might be hard to test
beaky 2017-02-28 10:50:06
dmwit hmm do those proof languages automagically do the 'test it a lot' thing for me
Ptival 2017-02-28 10:50:25
beaky: Coq has something called QuickChick that tries to do that
dmwit 2017-02-28 10:50:52
beaky: Generally, one proof is equivalent to infinitely many tests. So, yes, in a way.
dmwit 2017-02-28 10:51:10
beaky: The trick is you get all the fun of writing the proof. =)
Rupsbant_ 2017-02-28 10:51:24
I know, but if i use a user input and obfuscate the addition it should work i think
Ptival 2017-02-28 10:51:30
dmwit: I understood the question as "test it works before trying to prove" haha
Koterpillar 2017-02-28 10:51:32
there are infinitely many cases where infinitely many tests are worse than one proof
nshepperd_ 2017-02-28 10:51:32
I think i actually made a bst with compiler checked ordering once. For nats, using type level nats :0
Ptival 2017-02-28 10:51:39
but yeah, a proof is worth all tests
nshepperd_ 2017-02-28 10:51:48
But of course it was not very usable at all
Ptival 2017-02-28 10:52:32
Liquid Haskell is a good compromise for this, pretty sure the BST invariant would be easy for it to handle
Ptival 2017-02-28 10:54:45
cf. https://ucsd-progsys.github.io/liquidhaskell-tutorial/05-datatypes.html#/binarysearchtree
mniip 2017-02-28 10:56:16
Rupsbant_, are xmm insns susceptible to the issue too?
mniip 2017-02-28 10:57:35
because for double, ghc generates addsd+ucomisd
Rupsbant 2017-02-28 10:58:16
mniip the bug is noted in the list of haskell bugs
Rupsbant 2017-02-28 10:59:07
Let x = E1 in E2 may be different than E2[x/E1]
Rupsbant 2017-02-28 11:00:18
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/bugs.html#bugs-ghc
mbw 2017-02-28 11:13:26
K thanks for your help (before I forget).
Sonarpulse 2017-02-28 11:17:46
dolio: sorry for adding confusion with this "closing over" talk, that's separate forget about it
Sonarpulse 2017-02-28 11:18:17
dolio: I meant to include a condition that only functions may be the first argument of seq
Sonarpulse 2017-02-28 11:18:47
ack 4 4 `seq` \x -> x
Sonarpulse 2017-02-28 11:18:51
is no good then
Sonarpulse 2017-02-28 11:19:12
let n = ack 4 4 in \() -> n is also no good cause laziness
dolio 2017-02-28 11:20:10
"ack 4 4 `seq` \x -> x" is a function.
Sonarpulse 2017-02-28 11:20:36
dolio: sure, but I'm by fiat prohibiting non-function left of `seq`
dolio 2017-02-28 11:20:43
Why?
Sonarpulse 2017-02-28 11:20:51
that's too easy away to make some meaningful computation happen :)
Sonarpulse 2017-02-28 11:21:16
dolio: for background, I'm thinking about what I wrote in https://github.com/ghc-proposals/ghc-proposals/pull/27#issuecomment-283153349
Sonarpulse 2017-02-28 11:21:25
say all we had were unlifted functions
dolio 2017-02-28 11:21:45
It's easy to do without seq, too. It's just easiest with seq.
Sonarpulse 2017-02-28 11:22:12
if we only had those.....what would the downside be?
Sonarpulse 2017-02-28 11:22:43
explicit delaying with \() -> sucks
Sonarpulse 2017-02-28 11:23:16
but plain old exta expansion can delay any expression of type `a -> b` *without* changing the type!
Sonarpulse 2017-02-28 11:24:00
(similar with `let x = ... in (fst x, snd x)`)
Sonarpulse 2017-02-28 11:24:29
I'm thinking we should have always only had unlifted functions and products
Sonarpulse 2017-02-28 11:24:44
dolio: it may be easy, but I don't yet see it, care to show me?
Sonarpulse 2017-02-28 11:25:07
dolio: I can see doing big recursion with accumulator
Sonarpulse 2017-02-28 11:25:16
and then throwing away acumulator in base case
Sonarpulse 2017-02-28 11:25:20
(or closing over it)
dolio 2017-02-28 11:25:24
if even (ack 4 4) then (\x -> 1) else (\x -> 2)
Sonarpulse 2017-02-28 11:25:45
:)
Sonarpulse 2017-02-28 11:25:49
d'oh
Sonarpulse 2017-02-28 11:26:50
dolio: I was going to say "hmm still eliminating bool" but one can church-encode everything
mniip 2017-02-28 11:28:25
Sonarpulse, so you want product ADTs be strict by default?
mniip 2017-02-28 11:28:31
to be*
mniip 2017-02-28 11:29:12
but then [] would be unlifted
mniip 2017-02-28 11:29:22
and suddenly the ever-elegant [1..] is no more
dolio 2017-02-28 11:29:33
[] isn't a product.
mniip 2017-02-28 11:30:02
[](a) = 1 + a * [](a)
dolio 2017-02-28 11:30:21
And you don't need to be strict to be unlifted, just unable to distinguish bottom from a tuple of bottoms.
glguy 2017-02-28 11:31:28
mniip: The + there gives away that [] isn't a product
mniip 2017-02-28 11:31:40
okay what about Stream then
glguy 2017-02-28 11:31:58
that works fine, unlifted doesn't mean strict fields
mniip 2017-02-28 11:33:22
yeah but you can't tell bottom from bottom `Cons` bottom
glguy 2017-02-28 11:33:57
You'd only get to interact with it via head and tail, casing on the data constructor wouldn't "force" anything
mniip 2017-02-28 11:35:03
wouldn't that kinda imply having to provide all the elements' thunks upfront
codedmart 2017-02-28 11:39:58
any doctest users here? can you control the order of modules tested?
Squarism 2017-02-28 11:42:25
Not sure how i should think of this. I often find i have a dynamic datastructure where "i know" i have certain elements (because of prior checks) - but persist doing : fromJust $ M.lookup someKey mapContainingSomeKey. Any clean solutions to this?
johnw 2017-02-28 11:43:01
fromJust $ M.lookup key m = m M.! key
Squarism 2017-02-28 11:44:55
johnw, ? Not sure what you wrote there?
