yezariaely 2017-02-27 21:57:31
I have a function living in the IO monad and now I call the parsec parse function (which lives in another monad). How can I get them to work together? Do I need a monad transformer?
fendoer 2017-02-27 21:57:57
liftIO ?
liste 2017-02-27 21:58:03
yezariaely: what does the function do?
slack1256 2017-02-27 21:58:25
you can `runParse` and work with the value
fendoer 2017-02-27 21:59:07
:t liftIO
slack1256 2017-02-27 21:59:08
{ do ; let parsed = runParse scheme string ; print parsed }
lambdabot 2017-02-27 21:59:09
MonadIO m => IO a -> m a
fendoer 2017-02-27 22:01:08
> foo n = n * 2
lambdabot 2017-02-27 22:01:11
lambdabot 2017-02-27 22:01:11
parse error on input '='
lambdabot 2017-02-27 22:01:12
Perhaps you need a 'let' in a 'do' block?
fendoer 2017-02-27 22:01:16
> let foo n = n * 2
lambdabot 2017-02-27 22:01:21
mniip 2017-02-27 22:01:54
@let foo n = n * 2
lambdabot 2017-02-27 22:01:56
Defined.
fendoer 2017-02-27 22:03:03
> foo 4
lambdabot 2017-02-27 22:03:07
8
fendoer 2017-02-27 22:03:15
very cool, thanks :)
fendoer 2017-02-27 22:03:46
can i do IO stuff with the bot, too?
ongy 2017-02-27 22:07:36
no. that would be risky for the host of the bot
liste 2017-02-27 22:07:40
> putStrLn "hi" -- :)
lambdabot 2017-02-27 22:07:43
ongy 2017-02-27 22:08:00
> readFile "/etc/shadow"
lambdabot 2017-02-27 22:08:04
liste 2017-02-27 22:08:07
why don't they use the "safe" IO variant that try haskell uses?
fendoer 2017-02-27 22:08:14
so, he just ignroes you? ^^
liste 2017-02-27 22:08:28
fendoer: no, there's a Show instance for IO in the bot
liste 2017-02-27 22:08:39
so it doesn't execute the actions, it just shows them
ongy 2017-02-27 22:08:56
liste: o.0 what's that?
ongy 2017-02-27 22:09:03
not the show instance, "save" IO
liste 2017-02-27 22:09:15
ongy: http://chrisdone.com/posts/pure-io-tryhaskell
fendoer 2017-02-27 22:09:59
uhmmm.... what happened?
mauke 2017-02-27 22:10:23
matrix.org disconnected?
fendoer 2017-02-27 22:10:59
everyone just died?
mauke 2017-02-27 22:11:11
no, just people on matrix.org
fendoer 2017-02-27 22:11:26
i see, it happened on #Solus too
liste 2017-02-27 22:11:33
the whole Freenode
nshepperd_ 2017-02-27 22:11:55
When you die on matrix.org you die in real life
liste 2017-02-27 22:12:05
ouch, that's gonna be in the news soon
Theophane 2017-02-27 22:15:22
:')
fendor 2017-02-27 22:15:23
well, that joke's kinda good
Theophane 2017-02-27 22:15:50
sure it is
ongy 2017-02-27 22:17:05
IRC is real life
liste 2017-02-27 22:17:43
IRL is just a waste of time, IRC is real life
ongy 2017-02-27 22:18:22
who needs food when you can have lambdabot karma
ongy 2017-02-27 22:18:25
@karma
lambdabot 2017-02-27 22:18:25
You have a karma of 0
liste 2017-02-27 22:18:39
seems ongy's gonna need food after all
liste 2017-02-27 22:18:51
@karma edwardk
lambdabot 2017-02-27 22:18:51
edwardk has a karma of 55
liste 2017-02-27 22:19:11
(just checking that it hasn't been reset)
liste 2017-02-27 22:19:28
sorry for bothering :)
edwardk 2017-02-27 22:19:28
that number gets knocked around a lot
ongy 2017-02-27 22:20:10
you are a celebrity after all
edwardk 2017-02-27 22:20:31
its more the bot seems to have selective amnesia
ongy 2017-02-27 22:21:04
what was that quote? "If learning to program is like climbing a mountain, haskell is a brick wall, with edwardk building it higher and higher" (I think that was in one of the talks around lens?)
edwardk 2017-02-27 22:21:34
https://twitter.com/codemiller/status/695516883483828224
edwardk 2017-02-27 22:21:45
something katie posted to twitter once
edwardk 2017-02-27 22:22:39
i'm also partial to this one: http://imgur.com/TTBBeJs
fendor 2017-02-27 22:24:23
@karma
lambdabot 2017-02-27 22:24:24
You have a karma of 0
mauke 2017-02-27 22:24:41
@karma
lambdabot 2017-02-27 22:24:41
You have a karma of 60
fendor 2017-02-27 22:24:56
what does the karam determine?ß
fendor 2017-02-27 22:25:05
and lenses look cool :D
mauke 2017-02-27 22:25:11
how often someone's said "mauke++"
mauke 2017-02-27 22:25:23
austrian confirmed
Gurkenglas 2017-02-27 22:25:48
Germans also have that key there
mauke 2017-02-27 22:26:16
but they don't IRC from a tuwien host
merijn 2017-02-27 22:27:03
mauke: They could if they moved or had a conference ;)
edwardk 2017-02-27 22:27:03
fendor imaginary points on the internets
edwardk 2017-02-27 22:27:15
@karma shachaf
lambdabot 2017-02-27 22:27:15
shachaf has a karma of 97
tabaqui1 2017-02-27 22:27:19
@karma
lambdabot 2017-02-27 22:27:20
You have a karma of 0
ongy 2017-02-27 22:27:25
I should have more than 0 of those... at least if taken absolute
tabaqui1 2017-02-27 22:27:29
fendor++
fendor 2017-02-27 22:27:33
@karma
lambdabot 2017-02-27 22:27:34
You have a karma of 1
tabaqui1 2017-02-27 22:27:34
@karma fendor
merijn 2017-02-27 22:27:34
I remember walking through Vienna and randomly going "huh? Why do I have wifi?" only to find out I was automagically connecting to TU Wien :p
lambdabot 2017-02-27 22:27:34
fendor has a karma of 1
fendor 2017-02-27 22:27:38
yeah :D
tabaqui1 2017-02-27 22:27:38
hm
tabaqui1 2017-02-27 22:27:43
fendor--
fendor 2017-02-27 22:27:46
yeah eduroam is great :D
tabaqui1 2017-02-27 22:27:55
@karma fendor
lambdabot 2017-02-27 22:27:56
fendor has a karma of 0
tabaqui1 2017-02-27 22:28:10
@karma merijn
lambdabot 2017-02-27 22:28:11
merijn has a karma of 51
ongy 2017-02-27 22:28:44
hackage should have a feature: list packages by karma on #haskell
ongy 2017-02-27 22:28:49
@karma lens
lambdabot 2017-02-27 22:28:49
lens has a karma of 4
fendor 2017-02-27 22:29:01
@karma foldable
lambdabot 2017-02-27 22:29:02
foldable has a karma of 0
fendor 2017-02-27 22:29:09
@karma someRandomWord
lambdabot 2017-02-27 22:29:09
someRandomWord has a karma of 0
mauke 2017-02-27 22:29:16
@karma i
lambdabot 2017-02-27 22:29:16
i has a karma of 153
edwardk 2017-02-27 22:29:30
you know you can /msg lambdabot these queries ;)
ongy 2017-02-27 22:29:43
is karma not bound to the channel?
edwardk 2017-02-27 22:29:48
nope
fendor 2017-02-27 22:30:04
it should be bound to the bot, shouldnt it?
fendor 2017-02-27 22:30:40
i love that bot :D
fendor 2017-02-27 22:30:47
what else can he do?
edwardk 2017-02-27 22:31:03
she can do lots of stuff
edwardk 2017-02-27 22:31:11
@vixen a/s/l
lambdabot 2017-02-27 22:31:12
I'm glad I'm not Brezhnev. Being the Russian leader in the Kremlin. You never know if someone's tape recording what you say.
merijn 2017-02-27 22:31:49
vixen was removed
edwardk 2017-02-27 22:31:53
ah
merijn 2017-02-27 22:31:57
So it auto corrects to @nixon
edwardk 2017-02-27 22:32:01
heh
merijn 2017-02-27 22:32:14
Which, unlike, @vixen was not deemed politically incorrect enough to remove
edwardk 2017-02-27 22:32:21
fair
edwardk 2017-02-27 22:32:33
and now is oddly topical
edwardk 2017-02-27 22:32:43
well not for here
mniip 2017-02-27 22:33:12
! and edwardk
mniip 2017-02-27 22:33:16
an*
fendor 2017-02-27 22:35:04
why the hell does lambdabot has a brainfuck interpreter?
fendor 2017-02-27 22:35:09
*have
merijn 2017-02-27 22:35:13
fendor: Why not?
fendor 2017-02-27 22:35:25
ok, convinced, for the lolz?
edwardk 2017-02-27 22:35:31
lambdabot is sort of a community effort
mniip 2017-02-27 22:35:47
edwardk, is there a way to construct ends of Hask profunctors
edwardk 2017-02-27 22:35:50
lots of folks wrote lambdabot plugins as their first bit of haskell back circa 2006
mniip 2017-02-27 22:36:04
and is it possible to do in the Hask.hs framework?
ongy 2017-02-27 22:36:14
googling for the vixen plugin in lambdabot... why was that even a thing?
edwardk 2017-02-27 22:36:20
mniip: forall a. p a a is an end over p
fendor 2017-02-27 22:36:25
can one still submit code for the lambdabot?
mniip 2017-02-27 22:36:25
right
mniip 2017-02-27 22:36:32
but that's not really constructive
edwardk 2017-02-27 22:36:45
i don't know that i include it in the profunctors package
merijn 2017-02-27 22:36:53
fendor: I don't know who runs lambdabot currently, but if you convince said person to add it, sure
merijn 2017-02-27 22:37:09
fendor: You could also run your own copy of lambdabot, but you'll probably be asked not to do it here
edwardk 2017-02-27 22:37:09
what do you mean? it passes all the laws and by parametricity is forced to be the unique definition up to isomorphism
edwardk 2017-02-27 22:37:21
you can make a newtype wrapper for it if you must
edwardk 2017-02-27 22:37:24
same with coends
fendor 2017-02-27 22:37:51
merijn, ok, i bet there is a github repo?
mniip 2017-02-27 22:37:54
hmm
mniip 2017-02-27 22:38:04
maybe not Hask.hs framework is what I had in mind
mniip 2017-02-27 22:38:09
maybe closer to Generics
merijn 2017-02-27 22:38:18
fendor: https://hackage.haskell.org/package/lambdabot
fendor 2017-02-27 22:38:32
merijn, thanks
edwardk 2017-02-27 22:38:36
https://github.com/lambdabot/lambdabot
mniip 2017-02-27 22:38:48
if you have an algebraic construction of an ADT, can you obtain an algebraic description of the end of its profunctor?
edwardk 2017-02-27 22:38:54
mniip: still not sure what you are getting at
mniip 2017-02-27 22:39:26
edwardk, I'm not sure how common it is to represent ADTs as profunctors? if at all?
edwardk 2017-02-27 22:39:29
depends on if said adt has two type arguments and one of them is only in negative position
edwardk 2017-02-27 22:39:52
you may want to look up a couple of old papers
edwardk 2017-02-27 22:39:56
let me give you a reference
edwardk 2017-02-27 22:40:10
http://comonad.com/reader/2008/rotten-bananas/
edwardk 2017-02-27 22:40:32
that post is about separating out positive and negative occurences of a type variable in an ADT
edwardk 2017-02-27 22:40:36
and making it into a profunctor
edwardk 2017-02-27 22:40:41
i didn't use those words back then
mniip 2017-02-27 22:40:42
yeah
mniip 2017-02-27 22:40:44
exactly that
edwardk 2017-02-27 22:41:08
with that you can apply a trick from erik meijer to get a form of catamorphism/anamorphism
edwardk 2017-02-27 22:41:21
or you can use a more modern technique like used in the article that works better in practice
mniip 2017-02-27 22:41:32
"Λa. f a -> g a" turns into "Λa b. f b a -> g a b"
mniip 2017-02-27 22:41:35
and so on
edwardk 2017-02-27 22:42:01
anyways that article used the 'expfunctor' abstraction with one type variable, rather than a profunctor
edwardk 2017-02-27 22:42:06
later on i switched to a profunctor version
edwardk 2017-02-27 22:42:34
i think i wrote it up for a post about phoas for free or something
edwardk 2017-02-27 22:42:43
i don;'t remember if i ever fixed a couple bugs in that article though
edwardk 2017-02-27 22:42:53
yep
mniip 2017-02-27 22:43:25
is the integral notation intentional or just a coincidence
edwardk 2017-02-27 22:43:45
intentional, but the connection is kinda crappy to explain
mniip 2017-02-27 22:43:47
I mean the fact that we only bind one variable in the intergral and use it twice in the profunctor
edwardk 2017-02-27 22:44:52
well, what is positive and what is negative is "clear by context" to a mathematician, so they like to write less and maybe use little +/- signs to disambiguate
mniip 2017-02-27 22:45:47
somehow I don't like that
mniip 2017-02-27 22:46:13
is there a popular notation with two bindings?
edwardk 2017-02-27 22:46:22
most computer scientists get deeply uncomfortable at that point. most mathematicians get sore hands if they must be too explicit ;)
edwardk 2017-02-27 22:46:29
no
mniip 2017-02-27 22:46:38
damn
mniip 2017-02-27 22:46:45
anyway
edwardk 2017-02-27 22:46:58
in the right setting its just a limit anyways
mniip 2017-02-27 22:47:14
is there like, an algorithm to turn an ADT into the end ADT?
edwardk 2017-02-27 22:47:15
so you can reset your thinking so that it isn't even wrong
edwardk 2017-02-27 22:47:33
under certain assumptions of variance
mniip 2017-02-27 22:47:53
e.g
edwardk 2017-02-27 22:47:59
f (g x) -- is f co or contravariant?g?
mniip 2017-02-27 22:48:24
?
mniip 2017-02-27 22:48:51
once again, the ADT is described profunctorially
edwardk 2017-02-27 22:48:51
with derive Functor we just assume all 'f's in the type are Functors, and not Contravariant instances or something
edwardk 2017-02-27 22:49:09
i thought you wanted to generate the other way, nm
mniip 2017-02-27 22:49:17
the co and contravariant occurences of the tyvar are split
mniip 2017-02-27 22:49:35
and intertwined where appropriate
edwardk 2017-02-27 22:49:39
anywyas yes you could come up with something but we don't have Generic2
edwardk 2017-02-27 22:49:54
so you won't get a way to make the compiler write it for you
mniip 2017-02-27 22:50:14
what makes you so sure it's decidable?
edwardk 2017-02-27 22:51:14
converting to an one parameter version and taking a fixed point is a defineable thing in a language like haskell. in coq you're screwed
mniip 2017-02-27 22:51:19
also, I think, Generic1 probably contains enough information to reencode the ADT as a profunctor?
mniip 2017-02-27 22:51:24
and then you have tyfams
edwardk 2017-02-27 22:51:43
if you need to know where both parameters are plumbed, Generic1 is useless
edwardk 2017-02-27 22:52:24
and again, the whole thing needs assumption about which p's and q's are profunctors or bifunctors
mniip 2017-02-27 22:52:56
uh
edwardk 2017-02-27 22:52:58
that information isn't god given. with Functor deriving we just assume covariance. by the very nature o this you can't
mniip 2017-02-27 22:53:25
I'm not sure if you're following
mniip 2017-02-27 22:54:10
the idea is to take a *->* ADT and turn into into a profunctor *->*->*, with first arg guaranteed contravariant and second arg guaranteed covariant
mniip 2017-02-27 22:54:19
and such that the Join of that profunctor is the original ADT
edwardk 2017-02-27 22:54:36
data Foo p q f g a b = Foo (p (q (f a) (g b)) ()) -- if p is a bifunctor and q is a profunctor and f and g are functors then that is a profunctor.
mniip 2017-02-27 22:54:45
uh
mniip 2017-02-27 22:54:47
*->*
edwardk 2017-02-27 22:54:55
ok, so you're going the other way now
mniip 2017-02-27 22:55:05
not ((*->*)->(*->*))->(*->*)->(*->*)
mniip 2017-02-27 22:55:26
no like I mean
mniip 2017-02-27 22:55:30
suppose we have
mniip 2017-02-27 22:55:36
data Endo a = Endo (a -> a)
mniip 2017-02-27 22:55:41
using Generic1 we could make
mniip 2017-02-27 22:55:53
data EndoProfunctor a a' = Endo' (a -> a')
edwardk 2017-02-27 22:56:05
yes
mniip 2017-02-27 22:56:12
then, whether we can take the end of that is the question
mniip 2017-02-27 22:56:32
it should be iso to () but is there an algorithm for the general case
edwardk 2017-02-27 22:56:54
right up until i give you Compose, because you don't know if f and g in Compose are co or contravariant except by convention
mniip 2017-02-27 22:57:17
Compose doesn't, uh, break apart with Generic1
edwardk 2017-02-27 22:57:41
(:.:) is in GHC.Generics
edwardk 2017-02-27 22:57:44
or whatever
edwardk 2017-02-27 22:57:51
it'll let you drill in
mniip 2017-02-27 22:58:04
hmm
edwardk 2017-02-27 22:58:06
most people don't know how to use it, but its there
edwardk 2017-02-27 22:58:18
and you have to pick a stylized convention, e.g. that f is a Functor
edwardk 2017-02-27 22:58:42
that is the one caveat i'm pointing out
edwardk 2017-02-27 22:58:52
is that you have an algorithm up to assumptions of positive variance
mniip 2017-02-27 22:58:52
well
mniip 2017-02-27 22:58:54
type Rep1 ((:.:) f g) = D1 (MetaData ":.:" "GHC.Generics" "base" True) (C1 (MetaCons "Comp1" PrefixI True) (S1 (MetaSel (Just Symbol "unComp1") NoSourceUnpackedness NoSourceStrictness DecidedLazy) ((:.:) f (Rec1 g))))
mniip 2017-02-27 22:59:15
you mean how it recursively Rep1's g but not f?
edwardk 2017-02-27 22:59:45
you're looking at the Rep1 of (:.:), look at the Rep1 of (Compose f g)
edwardk 2017-02-27 23:00:04
thats like looking at Rep1 of U1 itself, not something that winds up using U1
edwardk 2017-02-27 23:00:25
but anyways, yes
mniip 2017-02-27 23:00:26
is that not derived?
edwardk 2017-02-27 23:00:46
its derived. but its just a level of misunderstanding waiting to happen
mniip 2017-02-27 23:00:54
anyway, let's ignore the implications of Generic1 mixed with polymorphism
edwardk 2017-02-27 23:01:10
once you drop polymorphism on the floor then the issue is boring
mniip 2017-02-27 23:01:18
well
edwardk 2017-02-27 23:01:19
you only have one source of contravariance (->)'s first argument
edwardk 2017-02-27 23:01:22
and so you can just tree walk
edwardk 2017-02-27 23:01:27
go nuts
mniip 2017-02-27 23:01:36
how do you propose to take ends of stuff with unknown variance?
edwardk 2017-02-27 23:01:39
and swap argument positions every time you recurse into the left of a (->)
edwardk 2017-02-27 23:01:52
what unknown variance. _everything_ is covariant other than the first argument of (->)
mniip 2017-02-27 23:02:04
no like I mean
mniip 2017-02-27 23:02:13
is it even possible to do in presence of polymorphism like you're describing
mniip 2017-02-27 23:02:52
'end_a f a a' is not even a valid statement if we don't know f is contravariant in first and covariant in second
edwardk 2017-02-27 23:02:59
ghc.generics itsef is predicated into breaking the world into sums, products, and some random decorations to spot constructors. it should also handle (->)'s but doesn't very well.
mniip 2017-02-27 23:03:14
1488276082 [13:01:22] and so you can just tree walk
edwardk 2017-02-27 23:03:20
yes, but you're taking a concrete ADT, and turning it INTO that.
mniip 2017-02-27 23:03:26
you mean to turn the adt into the profunctor representation
mniip 2017-02-27 23:03:31
yes, that's a tree walk
edwardk 2017-02-27 23:03:31
you only have to deal with the small handful of cases
mniip 2017-02-27 23:03:36
question is about the ends
edwardk 2017-02-27 23:03:38
and yes, because that is what you asked for
mniip 2017-02-27 23:04:00
can we similarly tree walk the end?
edwardk 2017-02-27 23:04:30
the tree construction you just asked for will make a profunctor. then you can take the end off it easy
mniip 2017-02-27 23:04:37
how?
edwardk 2017-02-27 23:04:47
forall a. f a a
mniip 2017-02-27 23:04:51
uh
mniip 2017-02-27 23:04:53
without that
edwardk 2017-02-27 23:05:07
that is literally what an end is in the category of haskell data types
mniip 2017-02-27 23:05:14
right
mniip 2017-02-27 23:05:29
but that doesn't give you a clue of what that type is
edwardk 2017-02-27 23:06:13
its an object with a series of morphisms from End f -> f a a for all the objects a in your category C.
mniip 2017-02-27 23:06:26
is it possible to construct 'forall a. f a a' with sums products exponents 1 and 0?
edwardk 2017-02-27 23:06:30
parametricity forces that to be one morphism with all those types
edwardk 2017-02-27 23:07:00
no. because the list of things provided by generics is incomplete
edwardk 2017-02-27 23:07:05
it doesn't handle quantification
edwardk 2017-02-27 23:07:25
no existentials, no universal quantification under ghc.generics
edwardk 2017-02-27 23:07:29
it doesn't understand such things
edwardk 2017-02-27 23:07:55
you can't make a rank-2 thing out of rank-1 parts in general
mniip 2017-02-27 23:07:57
if f is made up of sums, products, exponents, 1 and 0, can you do that
edwardk 2017-02-27 23:08:30
if you say so. i don't have such a construct in front of me
mniip 2017-02-27 23:08:56
also hm,
mniip 2017-02-27 23:09:10
so you say there's no universal algorithm to do that if f involves quantification?
edwardk 2017-02-27 23:09:19
i'm saying ghc.generics isn't up to the task
edwardk 2017-02-27 23:09:29
i'm not saying that you can't do something in a fancier language
mniip 2017-02-27 23:09:32
generics is kinda tangential to the question
mniip 2017-02-27 23:10:04
constructive constructions of ends is where I'm at
edwardk 2017-02-27 23:10:11
you can probably get some fancy self-describing thing in nice type theories like HoTT even when these start to include dependent types.
edwardk 2017-02-27 23:10:29
but you probably need induction-recursion
edwardk 2017-02-27 23:10:33
so meh
Aruro 2017-02-27 23:10:47
is Tagsoup capable of extracting tagpairs (open-close) together with their content?
Aruro 2017-02-27 23:11:03
like extract all
together with code itself edwardk 2017-02-27 23:11:16
i don't know once the type theory is weak enough that haskell is all you've got
mniip 2017-02-27 23:12:03
well
edwardk 2017-02-27 23:12:07
i'm just saying that forall a. f a a is a constructive construction in this type theory. it is a perfectly cromulent widget you can pass around. =)
mniip 2017-02-27 23:12:16
I'm mainly curious about the construction
edwardk 2017-02-27 23:12:21
you can refactor it into rank-1 parts some of the time
mniip 2017-02-27 23:12:24
forall a. f a a doesn't sound constructive
cocreature 2017-02-27 23:12:41
is there some json parser that accepts javascript notation, i.e., keys not enclosed in ""?
edwardk 2017-02-27 23:12:46
it doesn't sound rank-1
mniip 2017-02-27 23:12:56
maybe
edwardk 2017-02-27 23:13:01
but it works just fine and satisfies all the properties it is supposed to
mniip 2017-02-27 23:13:03
not sure what the precise definition is
mniip 2017-02-27 23:13:06
sure does
edwardk 2017-02-27 23:13:48
anyways the problem is i wind up with existentials and universals in all sorts of data types anyways, so they are part of my tools for describing the domain
edwardk 2017-02-27 23:14:16
that i can sometimes push stuff in and out of the quantifier until it disappears is a nicety, not something i expect to always get rid of it
edwardk 2017-02-27 23:14:23
its symbol pushing
edwardk 2017-02-27 23:14:33
if _that_ is the algorithm you are looking for, i don't know it
edwardk 2017-02-27 23:14:54
and i have no reason to expect the representation to be finite
mniip 2017-02-27 23:15:06
hmm
edwardk 2017-02-27 23:15:34
data Jet f a = a :- Jet f (f a)
mniip 2017-02-27 23:15:49
something something small caregories
edwardk 2017-02-27 23:15:56
has no finite representation in that form due to polymorphic recursion
mniip 2017-02-27 23:16:03
if we don't restrict ourselves to the category of small sets (types)
mniip 2017-02-27 23:16:14
then the naive forall a. f a a is a non-small quantification
edwardk 2017-02-27 23:16:26
you can make that thing above small enough by adding a base case.
edwardk 2017-02-27 23:16:54
but any number of distributive steps won't finish
mniip 2017-02-27 23:16:54
hm?
mniip 2017-02-27 23:17:07
ah
edwardk 2017-02-27 23:17:15
a :- f a :- f (f a) :- f (f (f a)) :- ...
mniip 2017-02-27 23:17:50
well it is expected that infinite adts might have infinite ends
mniip 2017-02-27 23:18:00
but they could still be algebraically described
mniip 2017-02-27 23:18:26
even though we can't tell 1 tree from seven
edwardk 2017-02-27 23:18:33
anyways, maybe you can find something suitable for representation in https://cs.appstate.edu/~johannp/tlca07-rev.pdf
mniip 2017-02-27 23:18:33
or was it four
edwardk 2017-02-27 23:19:10
seven
edwardk 2017-02-27 23:19:58
http://www.sciencedirect.com/science/article/pii/002240499500098H
edwardk 2017-02-27 23:20:12
there was a nice talk on the subject last year at lambdajam.au
edwardk 2017-02-27 23:21:04
anyways, i've blown all the energy i have tonight.
mniip 2017-02-27 23:21:45
cya
mniip 2017-02-27 23:21:47
thanks
[1]anon 2017-02-27 23:22:07
it has been great learning from you
f-a 2017-02-27 23:22:59
hello #haskell. I downloaded (let's say from github) a library cabal new-build it. The version of this particular is not present on hackage. Can I depend upon in on another project?
mniip 2017-02-27 23:23:54
but wait
mniip 2017-02-27 23:24:08
End Jet f = Void
mniip 2017-02-27 23:24:22
because Jet f a = a * ...
mniip 2017-02-27 23:24:48
and, I guess, end of a product is a product of ends?
Akii 2017-02-27 23:33:26
f-a: with stack you can add additional dependencies
Akii 2017-02-27 23:34:55
meh
Akii 2017-02-27 23:35:00
for the record http://lpaste.net/353051
Akii 2017-02-27 23:35:20
f-a: http://lpaste.net/353051
Akii 2017-02-27 23:35:24
with stack you can add additional dependencies
f-a 2017-02-27 23:37:58
thanks Akii
bollu 2017-02-27 23:39:44
how do I encode not (forall not a) in the type level?
bollu 2017-02-27 23:42:07
merijn: ^ any idea?
