Guest94118 2017-02-04 17:51:13
Hello, could anyone explain why in this example first function fails with <>, but second works http://pastebin.com/CG7P8ygh ? Thank you
dramforever 2017-02-04 17:55:33
Should use \~(_,_)
Guest94118 2017-02-04 17:56:02
Thank you! What is the meaning of ~?
dramforever 2017-02-04 17:56:28
Makes the pattern matching more lazy
dramforever 2017-02-04 17:56:47
'\~(x, y) -> e' is like '\xy -> let x = fst xy; y = snd xy in e'
dramforever 2017-02-04 17:57:05
In this way the argument will not be strictly evaluated
Guest94118 2017-02-04 17:57:38
Is this a GHC extention? I just added it to my code and and it didn't compile
dramforever 2017-02-04 17:57:39
In your case, \(_,_) causes the argument to be evaluated *before* the 'return (a, ())' kicks in
jle` 2017-02-04 17:57:48
@tell erisco implicitness is both a strength and a weakness :)
lambdabot 2017-02-04 17:57:48
Consider it noted.
jle` 2017-02-04 17:58:11
Guest94118: what's the error?
pavonia 2017-02-04 17:58:24
It's \ ~(_,_) with a space
Guest94118 2017-02-04 17:58:39
test.hs:7:16: error: parse error on input '\~'
dramforever 2017-02-04 17:58:57
Ahh, good catch
Guest94118 2017-02-04 17:59:18
Yes, adding space fixed it
Guest94118 2017-02-04 17:59:30
Everything works now! Thanks a lot!
dramforever 2017-02-04 17:59:32
> let (\~) = 2 in (\~)
lambdabot 2017-02-04 17:59:35
2
dramforever 2017-02-04 17:59:44
Totally unsurprising
Zemyla 2017-02-04 18:03:26
Hmm. If Haskell didn't have general lazy recursion, but did have folds, maps, and enumFromTo/enumFromThenTo, would that subset of the language be primitive recursive?
mniip 2017-02-04 18:12:24
if those are the only builtin functions then yes
mniip 2017-02-04 18:13:09
if you're careful enough to not allow infinite lists, you could say foldr is primitive recursive
erisco 2017-02-04 18:13:14
but why not this http://lpaste.net/352094
mniip 2017-02-04 18:13:23
trivially map is too, and enumFromTo is basically bounded recursion
erisco 2017-02-04 18:13:39
oh, because then promotion probably doesn't make sense
erisco 2017-02-04 18:13:46
@messages
erisco 2017-02-04 18:14:22
jle`, somewhat yes as I find it really difficult to keep the context in my head
erisco 2017-02-04 18:14:37
which is why I keep annotating
mniip 2017-02-04 18:15:10
erisco, haha
mniip 2017-02-04 18:15:19
add type Nat' = Nat
mniip 2017-02-04 18:15:22
and crash ghc
erisco 2017-02-04 18:15:34
does it? lol no thanks
erisco 2017-02-04 18:16:41
so, Sing is also just the proof terms for constructing data
mniip 2017-02-04 18:17:15
hehe I should test it with a recent ghc
erisco 2017-02-04 18:17:32
SZ is the proof that Z is a Nat, and so on
mniip 2017-02-04 18:18:35
erisco, I don't think you can have an infinite kind hierarchy that isn't *::*
erisco 2017-02-04 18:18:51
well yes, that would be the problem. I wasn't thinking about promotion
erisco 2017-02-04 18:19:11
it would only make sense if you employed special rules for it
jle` 2017-02-04 18:19:16
erisco: yeah, passing witnesses of contexts gives you more manual control
jle` 2017-02-04 18:19:21
and also lets you manipulate them as first-class values
jle` 2017-02-04 18:19:35
one of the common complaints with haskell's typeclass system is that typeclasses aren't first class, and they're magical/implicit
erisco 2017-02-04 18:19:53
existential type classes something something
jle` 2017-02-04 18:21:02
witnesses let you manipulate typeclasses and contexts as first-class values so there's a little bit of magic taken away
erisco 2017-02-04 18:21:07
also looking at Proxy... it is interesting
erisco 2017-02-04 18:22:01
such as why Sing (a :: Nat) and not just Proxy :: Proxy (a :: Nat)
dramforever 2017-02-04 18:22:20
Sing is for pattern matching
jle` 2017-02-04 18:22:35
erisco: if you pattern match on Proxy, it doesn't tell you anything about the type
dramforever 2017-02-04 18:22:36
You can't really pattern match Nat on the value level
erisco 2017-02-04 18:22:40
ah, I suppose that is true
erisco 2017-02-04 18:22:50
I was also going to say that Proxy doesn't give you any proof terms
dramforever 2017-02-04 18:23:03
Because that needs dependent types to work
erisco 2017-02-04 18:23:31
but the pattern matching is a significant difference
erisco 2017-02-04 18:23:41
so really, Proxy is not so appealing
dramforever 2017-02-04 18:23:55
Proxy doesn't do anything
erisco 2017-02-04 18:24:36
maybe you can get around having Proxy by using TypeApplications
erisco 2017-02-04 18:24:53
but that seems to be the purpose... to pass types
erisco 2017-02-04 18:25:04
Haskell doesn't have type parameters per se
mniip 2017-02-04 18:33:45
erisco, I might have a solution
erisco 2017-02-04 18:34:15
well, there is at least the Sing solution
erisco 2017-02-04 18:35:57
what was your thought mniip?
mniip 2017-02-04 18:36:54
oh hmmm
mniip 2017-02-04 18:37:19
I was thinking of using a constraint
mniip 2017-02-04 18:37:34
it didn't work too well
erisco 2017-02-04 18:40:30
there is just something amiss for me though... why do I have data Nat but data family := and data family :<
erisco 2017-02-04 18:40:48
why don't I need data := and a Sing wrapper for it
jle` 2017-02-04 18:42:48
where is := from?
erisco 2017-02-04 18:44:09
http://lpaste.net/352095
erisco 2017-02-04 18:44:43
I am stripping it back to just the fundamentals so I can get a grasp on it
jle` 2017-02-04 18:44:54
it looks like you're using a data family so that your := can be polymorphic
jle` 2017-02-04 18:45:07
but you really don't need one if you just want to do it for Nat's
