ph88 2017-01-30 11:55:29
what's this (Proxy :: Proxy f) ??
ph88 2017-01-30 11:56:03
looks like a type constructor with type signature
Koterpillar 2017-01-30 11:56:17
ph88: Nothing :: Maybe Int
Koterpillar 2017-01-30 11:56:22
ph88: same thing
Koterpillar 2017-01-30 11:56:40
ph88: the definition of Maybe is: data Maybe a = Nothing | Just a
Koterpillar 2017-01-30 11:56:48
ph88: the definition of Proxy is: data Proxy a = Proxy
jle` 2017-01-30 11:57:21
> (Nothing :: Maybe Int)
lambdabot 2017-01-30 11:57:24
Nothing
ph88 2017-01-30 11:57:28
how you know the definition of Proxy ?
jle` 2017-01-30 11:57:30
ph88: it's a value constructor with a type signature
jle` 2017-01-30 11:57:39
ph88: you can find the consturctors in the documentation for Proxy
jle` 2017-01-30 11:57:52
http://hackage.haskell.org/package/base-4.9.1.0/docs/Data-Proxy.html
ph88 2017-01-30 11:57:57
oh i thought Proxy was a type made up for that blog post
ph88 2017-01-30 11:58:01
didn't know it was on hackage
jle` 2017-01-30 11:58:09
ah no, it's actually included in 'base'/ghc
jle` 2017-01-30 11:58:16
like Int, Maybe, list, Either, etc.
ph88 2017-01-30 11:58:35
what is it used for ?
jle` 2017-01-30 11:58:43
situations like this
jle` 2017-01-30 11:58:46
:)
ph88 2017-01-30 11:58:50
lol
jle` 2017-01-30 11:59:10
it's a nice way to *pass* a 'type' as an input to a function
jle` 2017-01-30 11:59:20
er, 'pass' a *type*
ph88 2017-01-30 11:59:26
i always wanted to do that !
ph88 2017-01-30 11:59:36
can you match on type with Proxy ?
jle` 2017-01-30 12:00:02
not quite, it's mostly for the type checker
jle` 2017-01-30 12:00:14
as in, you're telling the type checker what type you want
jle` 2017-01-30 12:00:18
it doesn't actually carry the type at runtime
jle` 2017-01-30 12:00:28
for that you need things like Data.Dynamic/Data.Typeable or Data.Singletons
jle` 2017-01-30 12:00:54
basically sometimes the type checker might not be able to figure out what type you want to instantiate your function with, just from the inputs/outputs
jle` 2017-01-30 12:01:15
for simple functions like map :: (a -> b) -> [a] -> [b], for instance, it's pretty easy for the type checker to see what 'a' or 'b' you want
ph88 2017-01-30 12:01:27
where would it be useful to tell the type checker which type i want? If you would ask me this question i would just say use :: and you can tell the type checker which type you want
monochrom 2017-01-30 12:01:30
Proxy is most useful for instantiating return-type polymorphism.
jle` 2017-01-30 12:01:42
but for some functions, it's not possible to guess what you want your type variables to be from just the arguments/outputs
monochrom 2017-01-30 12:01:42
Err, no.
monochrom 2017-01-30 12:02:24
Proxy is most useful for instantiating parameterless polymorphism.
jle` 2017-01-30 12:02:26
ph88: if you wanted to implement like a SizeOf typeclass that gives how many byes a value of that type takes up in memory
jle` 2017-01-30 12:02:39
ph88: class SizeOf a where sizeOf :: Int wouldn't work
jle` 2017-01-30 12:02:41
do you see why?
jle` 2017-01-30 12:02:56
sizeOf :: Int ... how does the type checker know what type you want the size of?
jle` 2017-01-30 12:03:08
but imagine class SizeOf a where sizeOf :: Proxy a -> Int
jle` 2017-01-30 12:03:17
then you can do sizeOf (Proxy :: Proxy Bool)
jle` 2017-01-30 12:03:24
and that'll know that you want the Bool instance of sizeOf
ph88 2017-01-30 12:05:32
can't you just say sizeOf :: a -> Int ?
jle` 2017-01-30 12:05:44
sure, but that'll require you to actually pass a value of type 'a'
davean 2017-01-30 12:05:45
ph88: you'd need an 'a'
Koterpillar 2017-01-30 12:05:46
ph88: now we're back to passing undefined
davean 2017-01-30 12:05:50
where are you getting that 'a'?
jle` 2017-01-30 12:05:55
but what if you don't have a value of type 'a' available
jle` 2017-01-30 12:05:58
or you don't know how to make one?
monochrom 2017-01-30 12:06:33
"SizeOf a => a -> Int" causes people to believe that different values have different sizes.
davean 2017-01-30 12:06:45
which they sometimes do
monochrom 2017-01-30 12:06:55
"SizeOf a => Proxy a -> Int" says precisely to not expect that.
monochrom 2017-01-30 12:07:37
So between "a -> Int" and "Proxy a -> Int" you choose according to which message you want to convey. Or misconvey!
ph88 2017-01-30 12:08:11
oh you want to know the size of Bool and not a particular Bool .. right
monochrom 2017-01-30 12:08:32
So for a historical example, take a look at Storable in the FFI.
jle` 2017-01-30 12:09:10
there's also another common example Typeable, which is something close to a ShowType class
jle` 2017-01-30 12:09:22
class ShowType t where showType :: Proxy a -> String
jle` 2017-01-30 12:09:30
intance ShowType Bool where showType _ = "Bool"
jle` 2017-01-30 12:09:36
instance ShowType Int where showType _ = "Int"
monochrom 2017-01-30 12:09:42
It has "Storable a => a -> Int". But the intention is value independence, only type dependence. This was before we invented Proxy, so they had to say in the doc "it doesn't depend on the actual value!"
jle` 2017-01-30 12:10:01
then you can do showType (Proxy :: Proxy Int) and the type checker would know that you want 'Int'
monochrom 2017-01-30 12:10:07
And it becomes a source of misunderstanding to no end, because people don't read the doc.
glguy 2017-01-30 12:10:55
and then you generalize from: Proxy a -> String to proxy a -> String
ph88 2017-01-30 12:11:20
okay i'm mainly used to program on runtime, not on type-checker-time .. but i'll take it ShowType class is a good example
jle` 2017-01-30 12:13:55
yeah, it's basically a way of passing a type to the type checker at compiletime. passing types around at runtime is a whole different ordeal, heh
jle` 2017-01-30 12:14:04
since types are erased at runtime in haskell
monochrom 2017-01-30 12:15:44
When you use type classes too much, you're bringing types to run time.
ph88 2017-01-30 12:16:12
dictionaries right ?
monochrom 2017-01-30 12:16:56
That is an awful-lot-of-operational way to explain it, but yes.
ph88 2017-01-30 12:17:29
i'm all about operational :P
monochrom 2017-01-30 12:17:40
It doesn't scale.
ph88 2017-01-30 12:17:49
the reasoning ?
monochrom 2017-01-30 12:18:00
Yes.
ph88 2017-01-30 12:18:06
hows that ?
monochrom 2017-01-30 12:19:29
Suppose I give you a 500-line program that takes 3 hours to run, and ask you to understand it.
monochrom 2017-01-30 12:20:09
If your only technique is to run it in your head, it is going to take more than 3 hours. Because my "3 hours" assumes a 2GHz computer. Your head is slower than that.
ph88 2017-01-30 12:20:45
well you don't perform all calculations when reading the source code
exio4 2017-01-30 12:20:59
then you're not following operational semantics :)
monochrom 2017-01-30 12:21:00
That proves my point.
ph88 2017-01-30 12:21:26
i never meant it that literally :|
monochrom 2017-01-30 12:22:12
But you don't need dictionaries to explain why type classes bring types to run time either.
ph88 2017-01-30 12:22:38
i was already surprised about myself i could muster up 1 piece of relevant information
ph88 2017-01-30 12:22:57
but i'm sure there are lot's of other ways to explain it ^^
monochrom 2017-01-30 12:23:12
A faster explanation is to point at Data.Typeable and Data.Dynamic. They are also more useful immediately.
ph88 2017-01-30 12:24:23
using typeclasses too much + Typeable or Dynamic causes runtime overhead ?
monochrom 2017-01-30 12:24:37
What is overhead?
ph88 2017-01-30 12:24:45
anything on runtime really
monochrom 2017-01-30 12:24:59
Are you sure?
monochrom 2017-01-30 12:25:17
By now you know that I take your words very literally, you know. So, are you sure?
ph88 2017-01-30 12:25:26
in my book anything that is non essential to performing the algorithm as if it was implemented in assembly by the best of the best
monochrom 2017-01-30 12:25:43
OK, good, I agree with that.
monochrom 2017-01-30 12:25:56
Then the answer is "it depends".
ph88 2017-01-30 12:26:49
isn't it always ..
Rembane 2017-01-30 12:27:24
Will this give you analysis paralysis and anxiety and not letting you produce any code at all?
monochrom 2017-01-30 12:27:31
You're essentially asking: Is it true that every problem in the world can be solved without runtime type information.
Rembane 2017-01-30 12:27:57
monochrom: Is that a research area?
monochrom 2017-01-30 12:28:12
No. We already know that the answer is no.
ph88 2017-01-30 12:28:19
no ?
Rembane 2017-01-30 12:28:20
Oh. How disappointing.
hpc 2017-01-30 12:28:21
pick a language like idris and solve it at compile-time
Rembane 2017-01-30 12:28:29
monochrom: Why is it so?
ph88 2017-01-30 12:28:39
i thought things just had to be turing complete
monochrom 2017-01-30 12:28:42
I am too lazy to say why.
Rembane 2017-01-30 12:29:09
seq monochrom
ph88 2017-01-30 12:29:12
ok np
ph88 2017-01-30 12:29:17
i have to go to sleep
hodapp 2017-01-30 12:29:19
Rembane :P
monochrom 2017-01-30 12:29:30
My bet is that, for some problems, even if you solve by writing a Turing machine directly, you have an encoding of runtime type information somewhere.
hodapp 2017-01-30 12:29:36
ph88: Turing completeness actually isn't even a requirement of most things.
monochrom 2017-01-30 12:30:41
Take for example, if you do so much as write your own sql or nosql database, you have runtime type information.
AWizzArd 2017-01-30 12:30:57
I have foo n = let (Just f) = Just succ in f n – can this be made point-free? I tried removing the two occurrences of n.
ph88 2017-01-30 12:31:02
i think that be more on the level of, suppose your system handling personal registration and your type Sex can be Male or Female .. i'd just call it data, but w/e
jle` 2017-01-30 12:31:23
AWizzArd: foo = succ ...?
jle` 2017-01-30 12:31:43
what you wrote seems like foo = succ
AWizzArd 2017-01-30 12:31:47
Sure, it can be simplified like this, but I wonder if it is possible with the let syntax.
monochrom 2017-01-30 12:31:49
But all the world's problems are not solved by a personal registration system.
jle` 2017-01-30 12:32:00
AWizzArd: how do you want to use the let syntax?
ph88 2017-01-30 12:32:03
good night
AWizzArd 2017-01-30 12:32:19
I just wondered if it was possible or not.
jle` 2017-01-30 12:32:26
i'm not sure what you are looking for
jle` 2017-01-30 12:32:31
what part do you want to make point free?
glguy 2017-01-30 12:32:36
If you want to 1) be point-free, 2) use let syntax you end up with something like:
glguy 2017-01-30 12:32:38
foo = let {} in succ
monochrom 2017-01-30 12:32:47
foo = succ.
jle` 2017-01-30 12:32:49
the '(Just f) = Just succ' part?
jle` 2017-01-30 12:33:07
you might be misunderstanding what point free means
jle` 2017-01-30 12:34:10
it's just not quite clear what you're asking
monochrom 2017-01-30 12:35:41
Are you under a teacher who insists that you use "let"?
monochrom 2017-01-30 12:35:56
And did the teacher say "use it for real, don't f**k with me"?
glguy 2017-01-30 12:36:14
foo = do let{}; succ
AWizzArd 2017-01-30 12:41:54
monochrom: no teacher, just new to Haskell
monochrom 2017-01-30 12:42:20
OK good.
AWizzArd 2017-01-30 12:42:28
I just saw that the function returns f n, so maybe it can just return f.
AWizzArd 2017-01-30 12:42:56
foo = let (Just f) = Just succ in f -- looks okay to me, in principle.
ertes 2017-01-30 12:43:08
i wish there were Ord instances for things like IORef, MVar, etc.
monochrom 2017-01-30 12:43:09
Yes.
monochrom 2017-01-30 12:44:55
ertes: I think implementing Ord decreases efficiency.
