sveit 2017-02-24 10:55:44
so just to have some intuition, an "almost-trivial" data structure is the heap (used in priority queues). imperatively it's very easy to implement (have an array, append to the end and propagate up the "tree" for insertion (just swaps), and pop off an element to get the minimum). functionally I have seen some more complicated examples but is there a simple version with good asymptotics?
Tuplanolla 2017-02-24 10:56:11
Realistically `AF_INET`, `AF_INET6` and `AF_UNIX` are the only options, ongy.
ongy 2017-02-24 10:56:24
Tuplanolla: if only... if only....
sdrodge 2017-02-24 10:56:37
jle`: That seems like a weird way to describe ST. Would you mind clarifying what you mean?
Tuplanolla 2017-02-24 10:56:45
There's `AF_CAN` and other old stuff, but I couldn't even get the SocketCAN kernel module to cooperate with them, ongy.
jle` 2017-02-24 10:57:38
sdrodge: you describe an imperative algorithm by purely assembling imperative primitives
ongy 2017-02-24 10:58:17
I'm used to AF_PACKET and AF_NETLINK. But I those aren't in network
jle` 2017-02-24 10:58:17
using combinators like (>>=)
Cale 2017-02-24 10:58:17
http://hackage.haskell.org/package/psqueues provides some efficient priority search queues
lambdamu 2017-02-24 10:58:17
sveit: i don't think, in persistent datastructures you alwayes have to armotize a log factor away where imperatively you would have a constant
lambdamu 2017-02-24 10:58:17
*i dont think so
sveit 2017-02-24 10:58:17
something like "data Heap a = Node a (Maybe (Heap a)) (Maybe (Heap a))". Is this a "reasonable" way to implement a heap? My main problem is insertion. Do I have to do BFS to find the best insertion point every time?
jle` 2017-02-24 10:58:17
sveit: there's the skew heap, which is a pretty close relative to the normal heap, but is purely functional
sdrodge 2017-02-24 10:58:17
jle`: Okay, sure, but I wouldn't describe STRefs as being pure.
jle` 2017-02-24 10:58:35
sdrodge: im not sure if it makes sense to label them either way
lyxia 2017-02-24 10:58:39
sveit: you don't need a BFS for that.
jle` 2017-02-24 10:58:48
i'm talking about the method by which you describe an imperative algorithm
jle` 2017-02-24 10:58:52
you describe it purely
jle` 2017-02-24 10:59:07
using primivites like newSTRef, readSTRef, and combinators like (>>=), (<$>), etc.
sveit 2017-02-24 10:59:23
lyxia: how else do i find where to insert a node? if i just insert it at my first opportunity the tree will become unbalanced very quickly
sdrodge 2017-02-24 10:59:32
Surely you'd agree that readSTRef doesn't exhibit referential transparency, though.
erisco 2017-02-24 11:00:01
of course it does
dolio 2017-02-24 11:00:03
I wouldn't agree.
jle` 2017-02-24 11:00:52
' newSTRef >>= readSTRef ' returns the same imperative algorithm every time
jle` 2017-02-24 11:00:55
er, newSTRef x >>= readSTRef
jle` 2017-02-24 11:02:13
the description of the algorithm is done purely
erisco 2017-02-24 11:04:35
the whole point of these interfaces is that they work in a pure language
jle` 2017-02-24 11:04:35
the actual algorithm itself is imperative, or "impure"
jle` 2017-02-24 11:04:35
but the process of describing it is pure
lyxia 2017-02-24 11:04:35
sveit: I think you just need an integer to keep track of the size of the heap.
jle` 2017-02-24 11:04:35
you'd be in trouble if you used readSTRef on the same input, and then a different 'ST s a' came out every time
jle` 2017-02-24 11:04:35
or a different imperative program came out as a result every time
erisco 2017-02-24 11:04:35
just because something has side effects doesn't mean it isn't pure :P
lambdamu 2017-02-24 11:04:35
jle`: but couldn't the same be said about C doesn't you source code describe the same program every time?
jle` 2017-02-24 11:04:35
of course, >> doesn't commute, so 'x >> y' is different than 'y >> x' or 'x >> x >> y'
jle` 2017-02-24 11:04:35
but that's the same as 'x <> y' being different than 'y <> x' or 'x <> x <> y'
sveit 2017-02-24 11:04:35
lyxia: sure, then i would add to it every time i added an element. i meant i wanted something with the "minimal" data structure that I put.
jle` 2017-02-24 11:04:35
lambdamu: yes
Cale 2017-02-24 11:04:35
sveit: http://www.cs.ox.ac.uk/ralf.hinze/publications/ICFP01.pdf might be of interest -- it describes the implementation of a purely functional data structure for storing (priority, key) pairs, which acts both as an efficient priority queue, and can be searched by key.
erisco 2017-02-24 11:04:35
lambdabot, no. read uninitialized memory for example
jle` 2017-02-24 11:04:35
but you can't manipulate C source code progamatically very well
jle` 2017-02-24 11:04:35
it's definitely not as easy to manipulate as ST is
sdrodge 2017-02-24 11:04:35
Okay, maybe I'm missing something obvious, but consider newSTRef 4 >>= \x -> readSTRef x >> writeSTRef x 5 >> readSTRef x
jle` 2017-02-24 11:04:35
for sample 'x >> y' sequences two ST actions and performs them one after the other
lambdamu 2017-02-24 11:04:35
erisco: but even then isn't that just an effect? you can get a random number in haskell IO, too, e.g.
c_wraith 2017-02-24 12:00:34
all the ones I've seen have a very bad garbage collection story.
dmwit 2017-02-24 12:01:36
hah, ouch, yes
nitrix 2017-02-24 12:11:01
Having observed on #haskell-beginners that `and []` and `or []` can be understood as "Are all elements True" and "Is any element True", this made me think of forall and exists. What would be the notation for such propositions?
nitrix 2017-02-24 12:11:01
forall x. x `elem` xs, x == True
nitrix 2017-02-24 12:11:01
exists x. x `elem` xs, x == True
nitrix 2017-02-24 12:11:01
Do these seems like reasonable propositions? Also, it bothers me that the quantification is used to introduce values rather than types. Is this normal?
erisco 2017-02-24 12:13:12
:t and
lambdabot 2017-02-24 12:13:14
Foldable t => t Bool -> Bool
nitrix 2017-02-24 12:13:17
Besides, I'd like to explain that this is for the `and` and `or` functions and that `xs` is originating from a parameter. Is there a notation for that?
erisco 2017-02-24 12:13:41
∀x. x∈xs ⇒ x and ∃x. x∈xs ∧ x
erisco 2017-02-24 12:14:04
> or []
lambdabot 2017-02-24 12:14:07
False
erisco 2017-02-24 12:14:47
is that the kind of notation you were looking for?
nitrix 2017-02-24 12:15:40
erisco: That's familiar to me. I was more hoping for some :: alternative that'd like me express this relation inline.
erisco 2017-02-24 12:16:00
you mean you want these propositions as a type
nitrix 2017-02-24 12:16:00
e.g. and xs := forall x. x `elem` xs, x == True
nitrix 2017-02-24 12:16:43
erisco: Can it even exist at the type level? Proposing that all elements are True?
johnw 2017-02-24 12:16:44
have free arrows been made into a Hackage package yet?
erisco 2017-02-24 12:16:53
yes
nitrix 2017-02-24 12:18:00
erisco: How? Some sort of type equalities but with values?
nitrix 2017-02-24 12:18:05
Bool ~ True !? ahah.
nitrix 2017-02-24 12:18:29
Or a type whose only possible value is True?
erisco 2017-02-24 12:18:48
singletons and DataKinds will be involved
nitrix 2017-02-24 12:19:27
erisco: To be honest, I was originally curious how people expressed this denotationally, let's say, in a paper or similar, but now I'm also interested how I can propose this using the type system.
nitrix 2017-02-24 12:20:19
erisco: Do you mind sharing? Or I can actually experiment and see if I find the solution on my own?
erisco 2017-02-24 12:20:22
one way is to construct the lists which have the property
erisco 2017-02-24 12:20:49
or we can make a decision procedure that determines if a particular list has the property
nitrix 2017-02-24 12:21:42
I think I prefer constructing the list, as this gives us a proof, right?
erisco 2017-02-24 12:22:11
yes
nitrix 2017-02-24 12:22:48
erisco: Going home, I'll play a little and report on my progress :D
erisco 2017-02-24 12:23:00
good luck! :)
