bollu 2017-02-25 11:34:14
HoTT question: how is the expression refl_x . refl_x well typed? refl_x is an inhabitant of the type (x =A x) where (x : A). Hence, it makes no sense to talk about "composition of refl"
bollu 2017-02-25 11:34:23
so, like, what am I missing?
EvanR 2017-02-25 11:37:26
you can join paths from x to x with other paths to x to x
EvanR 2017-02-25 11:37:29
like you can compose id :: a -> a
EvanR 2017-02-25 11:38:27
with itself
EvanR 2017-02-25 11:41:13
or any other function from a to a
bollu 2017-02-25 11:45:26
EvanR: but according to HoTT, refl_x is _not_ a function, is it?
bollu 2017-02-25 11:45:27
it's an inhabitant of (x =A x)
EvanR 2017-02-25 11:45:27
no, its not function composition
bollu 2017-02-25 11:45:27
then?
bollu 2017-02-25 11:45:27
ohh
bollu 2017-02-25 11:45:27
it's a different operator for "path composition"?
EvanR 2017-02-25 11:45:27
its implication
bollu 2017-02-25 11:45:27
I don't see how
EvanR 2017-02-25 11:45:27
if a = b, and b = c, then a = c
EvanR 2017-02-25 11:45:27
"facts" of equality forms a category (and a groupoid thanks to symmetric property)
bollu 2017-02-25 11:45:27
no, I mean
EvanR 2017-02-25 11:45:27
the . you mentioned is the groupoid operation
bollu 2017-02-25 11:45:27
so, the type of the (.) operator is (a =A b) -> (b =A c) -> (a =A c) ?
bollu 2017-02-25 11:45:27
I see
EvanR 2017-02-25 11:45:27
yes
EvanR 2017-02-25 11:45:52
(conditionally, otherwise this sounds pointless)
Tuplanolla 2017-02-25 11:46:10
I don't see what you mean.
EvanR 2017-02-25 11:46:28
what do you want to happen if socketToHandle fails
Tuplanolla 2017-02-25 11:46:46
That would result in `close sock`.
EvanR 2017-02-25 11:46:57
and is accept fails?
EvanR 2017-02-25 11:47:02
and if*
Tuplanolla 2017-02-25 11:47:04
I meant `close conn` there.
Tuplanolla 2017-02-25 11:47:15
Accept failing would result in `close sock`.
Tuplanolla 2017-02-25 11:47:57
A failure at a later point would result in `hClose hand` and `close sock`, but not `close conn`.
EvanR 2017-02-25 11:48:20
jeez
EvanR 2017-02-25 11:48:40
dont ever close anything
EvanR 2017-02-25 11:48:54
in all your handlers, throw an indicator of what fails, and interpret it at the outside
Tuplanolla 2017-02-25 11:48:56
The point is that `socketToHandle` changes one release operation to another and that's awkward.
EvanR 2017-02-25 11:49:06
throw a bitmask of what to close
EvanR 2017-02-25 11:49:18
then you can close any combination of things once
EvanR 2017-02-25 11:50:14
in idris, theres this state machine encoded into the types of where you are in the process, giving you full control over what should happen when
EvanR 2017-02-25 11:50:39
so you can do a sequential logic style state machine diagram to figure out how it should work ;)
EvanR 2017-02-25 11:51:04
doesnt sound like bracket works
Tuplanolla 2017-02-25 11:51:49
Let's see if I can draft a type for the function that does the mapping thing.
swolffs 2017-02-25 11:53:38
so, I recently learned it's supposedly possible to write this:
swolffs 2017-02-25 11:53:48
instance Monad m => Applicative m
EvanR 2017-02-25 11:54:26
every monad can be equipped with <*> in the dumbest possible way, using >>=
swolffs 2017-02-25 11:54:32
and I know that instance can actually be written if the compiler accepts that first line
EvanR 2017-02-25 11:54:45
by using ap
swolffs 2017-02-25 11:55:02
EvanR: so... it's an optimisation issue?
EvanR 2017-02-25 11:55:25
you cant write that because it would be overlapping instances
swolffs 2017-02-25 11:56:20
sorry, I didn't mean "I learned >>= can construct <*>", I knew that. I meant that someone claimed that top-level context restrictions on instances are apparently now OK
EvanR 2017-02-25 11:56:46
huh, what do you mean by top level here
glguy 2017-02-25 11:57:00
swolffs: Yes you can write that syntax; no, it probably doesn't mean what you hope it does
swolffs 2017-02-25 11:57:21
what I hope it does is...
glguy 2017-02-25 11:57:53
Not conflict with every other Applicative instance
swolffs 2017-02-25 11:58:19
sec, let me rewrite the Idris code to be syntactic Haskell
swolffs 2017-02-25 11:58:35
ah
swolffs 2017-02-25 11:58:41
right
swolffs 2017-02-25 11:58:41
so Haskell does *not* have overload conflict resolution
swolffs 2017-02-25 11:58:41
thanks
EvanR 2017-02-25 11:58:41
it does have ways to control overlapping instances, with extensions
EvanR 2017-02-25 11:58:41
but i am scared by it
swolffs 2017-02-25 11:58:41
I always took that to be the reason Haskell does "class Applicative m => Monad m"
swolffs 2017-02-25 11:58:53
which, if you could actually resolve the conflicts safely and easily, would be a weird restriction
swolffs 2017-02-25 11:59:22
but if conflicts cause serious issues, the current approach seems a sensible compromise
EvanR 2017-02-25 11:59:31
normally the resolution process requires a unique instance to choose
EvanR 2017-02-25 11:59:44
idris doesnt have that restriction
swolffs 2017-02-25 11:59:46
yeah, that's how I understood it
swolffs 2017-02-25 11:59:48
yeah
swolffs 2017-02-25 12:00:03
but Idris does copy the "class Applicative m => Monad m"
swolffs 2017-02-25 12:00:30
and I suspect that's copying a restriction without understanding the original reason, which no longer applies
swolffs 2017-02-25 12:01:26
but I can't be sure
c_wraith 2017-02-25 12:01:26
That's less of a restriction and more of a statement of truth
EvanR 2017-02-25 12:01:26
that means to build a Monad, you need to provide an Applicative on the same argument type
EvanR 2017-02-25 12:01:26
(in idris)
swolffs 2017-02-25 12:01:26
c_wraith: that depends whether your logic is classical
swolffs 2017-02-25 12:01:28
c_wraith: it's true in classic logic, sort of
c_wraith 2017-02-25 12:01:31
swolffs: it's constructive, given that we're programming
swolffs 2017-02-25 12:01:42
c_wraith: correct. Therefore, it's false
c_wraith 2017-02-25 12:01:45
swolffs: the construction is pure = return, (<*>) = ap
swolffs 2017-02-25 12:01:57
c_wraith: I know
EvanR 2017-02-25 12:01:58
instance Monad m => Applicative m means that all Applicatives will be implemented in terms of monads
EvanR 2017-02-25 12:02:03
or a constant implementation
c_wraith 2017-02-25 12:02:08
swolffs: so.. there's a constructive proof
swolffs 2017-02-25 12:02:14
that's the truth of "instance Monad m => Applicative m"
swolffs 2017-02-25 12:02:40
what I'm saying is that "class Applicative m => Monad m" is only equivalent classically
EvanR 2017-02-25 12:02:58
instance and class arent saying anything comparable
c_wraith 2017-02-25 12:03:00
Oh. That's *not* an impication
c_wraith 2017-02-25 12:03:06
*implication
swolffs 2017-02-25 12:03:08
I know
EvanR 2017-02-25 12:03:09
class Applicative m => Monad m isnt a restriction
swolffs 2017-02-25 12:03:14
it's an anti-implication
EvanR 2017-02-25 12:03:46
since you can always get a free instance if you cant think of anything
swolffs 2017-02-25 12:03:54
EvanR: it complains if I define instance Monad MyType without adding instance Applicative MyType. Seems like a restriction
EvanR 2017-02-25 12:04:08
its not stopping you from doing anything
EvanR 2017-02-25 12:04:31
it would be nice if the additional instance could be generated with a flag
swolffs 2017-02-25 12:04:35
sec, I'm testing this
EvanR 2017-02-25 12:04:37
besides that its trivial
swolffs 2017-02-25 12:04:42
right
EvanR 2017-02-25 12:05:39
it barely ever works
lielazive 2017-02-25 12:05:40
How do I repopulate stack's package list? It thinks the latest package is directory-1.2 not 1.3
EvanR 2017-02-25 12:06:01
having more stuff for it to fail to disambiguate would only make it worse
EvanR 2017-02-25 12:06:46
but theres a dedicated idris channel
swolffs 2017-02-25 12:06:52
EvanR: so... no trying that unless and until resolution is more robust
swolffs 2017-02-25 12:07:11
EvanR: I know. They sent me here to ask about the why of "class Applicative m => Monad m"
swolffs 2017-02-25 12:07:26
which I now have, so I'll head back
EvanR 2017-02-25 12:07:27
the best way to get it to resolve stuff is to have only 1 choice (kind of defeating the purpose)
swolffs 2017-02-25 12:07:29
thanks
EvanR 2017-02-25 12:08:13
oh, was that the question
EvanR 2017-02-25 12:08:49
didnt realize
EvanR 2017-02-25 12:10:00
class Applicative m => Monad m was a breaking change made relatively recently, and while its interesting, i cant answer why it was done
swolffs 2017-02-25 12:10:20
EvanR: it was, but I got carried away
glguy 2017-02-25 12:10:21
All the types with Monad instance should have Applicative instances, having "class Applicative m => Monad m" means that we don't need a redundant "Applicative" instance to use applicative operations when we have a Monad instance around
swolffs 2017-02-25 12:10:22
I have my suspicions about the why, if conflict resolution can only be done by "scary" language extensions
glguy 2017-02-25 12:10:44
So if you have some definition :: Monad m => m this -> that, it saves you from also needing an Applicative m constraint
EvanR 2017-02-25 12:11:09
ah
swolffs 2017-02-25 12:11:11
glguy: that's the wrong way around I think: "class Applicative m => Monad m" means you can't even define a Monad instance without defining a (redundant) Applicative instnace
glguy 2017-02-25 12:11:22
No, it's what I said
swolffs 2017-02-25 12:11:27
oh, right, the second is what I understood
glguy 2017-02-25 12:11:37
when you define a Monad instance you will in fact also need an Applicative instance
swolffs 2017-02-25 12:11:47
it cuts down on instances of functions
glguy 2017-02-25 12:11:49
but often it's better to implement that instance directly
swolffs 2017-02-25 12:12:00
but it increases instances of Applicative
glguy 2017-02-25 12:12:01
than to derive it
swolffs 2017-02-25 12:12:34
because of speed?
glguy 2017-02-25 12:13:07
yeah, you can write a more efficient implementation
EvanR 2017-02-25 12:13:19
the number of types that *are* applicative remains the same
EvanR 2017-02-25 12:13:23
as before, you just get a more uniform api
