taktoa 2017-02-24 08:45:41
cdidd: only principal types, which you really should be annotating anyway
dolio 2017-02-24 08:54:20
That's not what "principal types" means. :)
flxw 2017-02-24 08:59:09
Hi all. I'd liketo ask a theory question. The idea of free theorems seems usually to be expressed using logical relations and parametricity. I have no experience with either of them. Lately someone mentioned in passing, that the free theorems idea could be explained using natural transformations as well. So as a concrete question: What kind of categorical setting would one need to show that id: a -> a has a unique inhabitant, nam
flxw 2017-02-24 08:59:09
x = x (modulo bottoms to make it easier for starters like me)?
monochrom 2017-02-24 09:00:34
There will be many different things, all called "identity" confoundingly, in this example.
monochrom 2017-02-24 09:01:07
id is a natural tranformation from the Identity functor to the Identity functor.
dolio 2017-02-24 09:01:22
I'm not sure the person was exactly telling you the truth.
dolio 2017-02-24 09:01:45
The free theorem for that type tells you that `id` is natural.
dolio 2017-02-24 09:02:24
But the reason for inventing naturality is that not all definable operations with that 'type' in mathematics are natural.
robertkennedy 2017-02-24 09:02:46
Philip Wadler's "Category Theory for the Working Hacker" talk proves that `(,) <$> fst <*> snd` is unique. Maybe look at that?
monochrom 2017-02-24 09:03:15
So, for all object A, id_A :: Identity A -> Identity A, which is a long way to say id_A :: A -> A, but you need to insert the Identity functor to see functors.
lambdamu 2017-02-24 09:05:00
maybe he was confusing free theorems with free constructions which arise from adjunctions which are certain functors related by natural transformations
flxw 2017-02-24 09:05:34
Oh, I see. Yes, id must be many things, if it's to become a natural transformation, one component for each type a.
dolio 2017-02-24 09:08:32
I suppose if you understood what naturality is, you could get some idea of free theorems from 'this operation is natural in a way related to the type', instead of thinking about relations related to the type.
dolio 2017-02-24 09:08:37
If that's what is meant.
flxw 2017-02-24 09:08:37
Yes, I'll have a look at wadler's talk. And as it seems, getting better acquainted with LR und parametricity will be unavoidable when I want to understand the free theorem stuff better ...
dolio 2017-02-24 09:09:21
There are types that aren't easy to see in those terms, though.
flxw 2017-02-24 09:09:43
dolio: yes, I meant it in that sense.
flxw 2017-02-24 09:10:34
as a start I'd be completely happy with seeing some types. Dosn't need to be all of them at once. :-)
EvanR 2017-02-24 09:11:08
cantors diagonal argument uses the notion of a listing of reals (in the form of digit sequences), and the notion of a listing which is complete. by assuming a complete listing you get a contradiction by constructing a witness to its incompleteness. So a complete listing is contradictory. However an incomplete listing is OK, and the diagonal construction still works for generating a "new" real. this process
EvanR 2017-02-24 09:11:14
can be iterated indefinitely, prepending each new real to the beginning of the listing. will this process eventually reach all reals?
monochrom 2017-02-24 09:11:59
That's the continuum hypothesis.
EvanR 2017-02-24 09:13:16
it is?
monochrom 2017-02-24 09:15:35
I am taking "eventually" very liberally. But the next cardinal after the naturals is continuum-hypothesized to be the reals.
dolio 2017-02-24 09:16:32
I don't think that question is answered by the continuum hypothesis.
lambdamu 2017-02-24 09:17:39
is any question answered by the continuum hypothesis?
dolio 2017-02-24 09:18:50
I don't think it's specified clearly enough to answer, either, though.
EvanR 2017-02-24 09:18:54
i guess i should try to write the haskell code for that and see what happens
monochrom 2017-02-24 09:20:02
There are a few more words I need to say. The process looks more like ordinals than cardinals. But that difference can be bridged. The first uncountable ordinal = the first uncountable cardinal anyway.
EvanR 2017-02-24 09:20:25
type error
dolio 2017-02-24 09:20:36
How are you going to get to the first uncountable ordinal by adding 1 to countable ordinals?
dolio 2017-02-24 09:20:40
Repeatedly.
monochrom 2017-02-24 09:21:04
Oh yikes.
monochrom 2017-02-24 09:22:22
But Haskell code is not going to help. Any haskell program (any program in any language) can only be run for less than omega steps. You can't even observe the first time you add an extra real number.
dolio 2017-02-24 09:22:29
Also, what counts as a "listing", and are you sure that what you're doing with ordinals counts?
Aruro 2017-02-24 09:22:38
is there github repo mirroring wiki.haskell.org?
EvanR 2017-02-24 09:24:16
a listing of reals (in the form of digit sequences) is a function from N to N to D where D is the type of digits
EvanR 2017-02-24 09:24:55
so an infinite matrix
EvanR 2017-02-24 09:25:20
you can prepend to it like hilberts hotel
EvanR 2017-02-24 09:25:25
(in 2 directions)
EvanR 2017-02-24 09:25:44
thats what i expected, if you attempt to list all reals somehow, you ought not to be able to even get started
dolio 2017-02-24 09:26:20
Okay, so what does "eventually reach all reals" mean?
ripread 2017-02-24 09:26:22
Hey, Haskell newbie here. I'm having trouble getting recursion to work in ghci. ghci --version = 8.0.1.
ripread 2017-02-24 09:26:38
ghci> rec 0 = 1
ripread 2017-02-24 09:26:47
ghci> rec n = n + rec (n-1)
ripread 2017-02-24 09:26:53
ghci> rec 5
Tuplanolla 2017-02-24 09:26:53
The second line shadows the first one, ripread.
EvanR 2017-02-24 09:27:00
i guess it ends up being the same thing, technically, as being complete
dolio 2017-02-24 09:27:45
Having a complete listing?
monochrom 2017-02-24 09:28:31
I recommend you to put code in file and use :load. It's much simpler and editable.
EvanR 2017-02-24 09:30:09
so the process doesnt add anything new to the situation, despite adding infinite new things
ripread 2017-02-24 09:30:09
Tuplanolla is that something specific to the repl? cause they have very similar recursive code in LearnYouAHaskell
monochrom 2017-02-24 09:30:09
But if you insist, "let {rec 0 = 1; rec n = n + rec (n-1)}
EvanR 2017-02-24 09:30:09
however you can take the output of that process, and feed it into a second copy of itself to get even more new reals
EvanR 2017-02-24 09:30:09
and so on
Tuplanolla 2017-02-24 09:30:09
Shadowing is universal, ripread.
EvanR 2017-02-24 09:30:09
and repeat that indefinitely
EvanR 2017-02-24 09:30:09
so higher order computability like
lyxia 2017-02-24 09:30:09
ripread: if you insist on making it multiline http://lpaste.net/352948
Tuplanolla 2017-02-24 09:30:09
It's just that the top level in files and the prompt in GHCi are different contexts, ripread.
monochrom 2017-02-24 09:30:09
Also pretty sure LYAH tells you to use a file.
EvanR 2017-02-24 09:30:09
maybe not because the first level never gives you a listing with a beginning
EvanR 2017-02-24 09:30:09
ah so thats different
EvanR 2017-02-24 09:31:25
it generates a zipper, one way is the original incomplete listing and the other direction is the unfolding by diagonal manipulation
EvanR 2017-02-24 09:31:41
in that way you can observe it
contiver 2017-02-24 09:35:14
What's the usual consensus when uploading a package to hackage? Should the Text/Data/Control/ etc. structure be respected, or is it ok to upload something outside it (such as the Pipes library does)? I've been told that as long as the name isn't a generic one (say, Parser), it's fine.
contiver 2017-02-24 09:35:31
But it is my first time uploading something to Hackage, so I'm trying to avoid messing it up.
Tuplanolla 2017-02-24 09:35:36
What's the name, contiver?
contiver 2017-02-24 09:35:40
Hasmin
Tuplanolla 2017-02-24 09:36:33
I wouldn't care.
byorgey 2017-02-24 09:38:12
contiver: my sense is, Text/Data/Control is appropriate if and only if you are uploading a library which contains some sort of fundamental data structure or abstraction.
myfreeweb 2017-02-24 09:38:39
There was a "do not use Text/Data/Control in your packages" post on /r/haskell recently i think
byorgey 2017-02-24 09:39:25
for most things, I would not recommend putting your modules in those namespaces. Pick whatever makes sense.
Tuplanolla 2017-02-24 09:39:25
Then again `Game.Hasmin` would make sense.
myfreeweb 2017-02-24 09:40:16
Com.Contiver.Packages.Games.Hasmin.HasminApp :D
EvanR 2017-02-24 09:42:56
Everything.EverythingReal.ProgrammingLanguageLibraries.Haskell....... .
EvanR 2017-02-24 09:42:58
someyhing
contiver_ 2017-02-24 09:43:45
so I'm guessing people will be fine with it?
monochrom 2017-02-24 09:43:48
Quaternion.Complex.Real.Integer.Natural.Programming.Haskell.Data.Double
nshepperd_ 2017-02-24 09:44:10
I think do whatever you like as long as you don't collide with anything
contiver_ 2017-02-24 09:44:31
good. Thanks for the answers :)
mauke 2017-02-24 09:44:38
Comp.Lang.Haskell
