maybefbi 2017-02-22 01:45:21
Jinixt, perhaps then you could use such a list as the leaf of your tree
Jinixt 2017-02-22 01:45:25
nah, given a data structure, i want to search and replace sub-structures
Jinixt 2017-02-22 01:45:46
yeah, that's what i had in my original example :)
maybefbi 2017-02-22 01:46:46
lyxia, so there are more folds than just Foldable
ertes 2017-02-22 02:17:09
maybefbi: the term "fold" is overloaded, but one well-defined notion of it comes from category theory: what lyxia said
maybefbi 2017-02-22 02:17:24
ertes, copy that
ertes 2017-02-22 02:18:01
maybefbi: it has two main characteristics: 1. it's fully information-preserving, so you can reconstruct the original data structure (the identity fold)
ertes 2017-02-22 02:18:12
like: foldr (:) []
ertes 2017-02-22 02:18:24
2. it does nothing "extra"
max3 2017-02-22 02:18:43
is there a way to throw an exception that identifies itself showing line number and source file it came from?
ertes 2017-02-22 02:19:06
so a fold is the "smallest possible" recursive function that can recover the full data structure
maybefbi 2017-02-22 02:19:14
ertes, one of the examples my interviewer showed me had 3 arguments unlike (:)
ertes 2017-02-22 02:19:29
that's fine… a fold can result in a function
athan 2017-02-22 02:19:33
max3: there's a constraint for it iirc, like WithCallsite or something
max3 2017-02-22 02:20:14
athan, what do you mean by constraint?
ertes 2017-02-22 02:20:14
> foldr (\x xs n -> if n > 0 then x : xs (n - 1) else []) (pure []) "abcdefg" 3
lambdabot 2017-02-22 02:20:18
"abc"
ertes 2017-02-22 02:20:26
maybefbi: ^ 'take' in terms of foldr
ertes 2017-02-22 02:20:45
maybefbi: http://ertes.eu/tutorial/foldr.html#stateful-folds
maybefbi 2017-02-22 02:21:16
ertes, yeah we weren't talking about anything :: (Foldable t)..
maybefbi 2017-02-22 02:22:25
e.g. i was asked to implement foldr for Maybe a
maybefbi 2017-02-22 02:22:41
and the first parameter of said fold was a function :: (a -> b)
maybefbi 2017-02-22 02:23:32
here is how the interview started:
maybefbi 2017-02-22 02:23:50
Him: write a data type
maybefbi 2017-02-22 02:23:54
Me: data Void
maybefbi 2017-02-22 02:24:04
Him: write foldr for it
maybefbi 2017-02-22 02:24:27
Me: I can write one but you cannot call it foldr _ _ _ = undefined
maybefbi 2017-02-22 02:24:47
Him: yes this is technically correct. write another data type.
ertes 2017-02-22 02:24:49
maybefbi: do you know what the fold for Void is?
athan 2017-02-22 02:25:01
max3: ahh here we go: https://hackage.haskell.org/package/call-stack-0.1.0/docs/Data-CallStack.html#v:callStack
ertes 2017-02-22 02:25:02
at least its type
maybefbi 2017-02-22 02:25:19
ertes, yes i know its type. it is:
maybefbi 2017-02-22 02:25:43
ertes, foldr :: (a -> b -> b) -> b -> Void -> b
ertes 2017-02-22 02:25:47
maybefbi: nope
ertes 2017-02-22 02:25:58
foldVoid :: Void -> r
ertes 2017-02-22 02:26:18
that's the Void fold, and surprisingly enough it's a well-defined function
ertes 2017-02-22 02:26:32
which, unfortunately, you can't write in standard haskell without cheating =)
maybefbi 2017-02-22 02:26:34
i agree it is well-defined although no one can call it
ertes 2017-02-22 02:26:37
but you can write it with -XEmptyCase
maybefbi 2017-02-22 02:26:44
oh cool
maybefbi 2017-02-22 02:27:25
ertes, why isn't foldVoid :: (a -> b -> c -> d) -> e -> Void -> f ?
maybefbi 2017-02-22 02:27:35
because i can still write its definition
maybefbi 2017-02-22 02:27:46
foldVoid _ _ _ = undefined
max3 2017-02-22 02:28:18
i guess because of "Deprecated: error appends the call stack now" error is good enough
ertes 2017-02-22 02:28:28
maybefbi: the true type for the Void catamorphism is the following: foldVoid :: (F r -> r) -> Fix F -> r
ertes 2017-02-22 02:28:39
maybefbi: can you come up with an F such that Fix F = Void?
maybefbi 2017-02-22 02:29:27
ertes, ok if you say so. because i did not know about catamorphisms back then. to be folds can only be defined for container like things
athan 2017-02-22 02:29:29
max3: oh jeez sorry haha
maybefbi 2017-02-22 02:29:48
ertes, i cannot come up with F such that Fix F is Void
ertes 2017-02-22 02:29:58
maybefbi: folds can be defined for any type that is the least fixed point of a type function
ertes 2017-02-22 02:31:22
maybefbi: newtype Fix f = Fix { fromFix :: f (Fix f) }
ertes 2017-02-22 02:31:22
data VoidF x
ertes 2017-02-22 02:31:22
VoidF (Fix VoidF) ≃ 0
ertes 2017-02-22 02:31:22
where 0 is the empty type
maybefbi 2017-02-22 02:31:34
i didn't know about 0 until just now
ertes 2017-02-22 02:31:47
maybefbi: with that in mind the Void fold has this type: (VoidF r -> r) -> Fix VoidF -> r
ertes 2017-02-22 02:32:18
now apply some type algebra:
ertes 2017-02-22 02:32:30
(VoidF r -> r) -> Fix VoidF -> r
ertes 2017-02-22 02:32:34
(0 -> r) -> Fix VoidF -> r
ertes 2017-02-22 02:32:41
() -> Fix VoidF -> r
ertes 2017-02-22 02:32:44
Fix VoidF -> r
ertes 2017-02-22 02:33:14
and Void ≃ Fix VoidF, which leaves you with: Void -> r
maybefbi 2017-02-22 02:34:21
this is news to me.
maybefbi 2017-02-22 02:35:19
it seems everything i learn has a more permissible and more abstract version of it, with a truer meaning
maybefbi 2017-02-22 02:35:39
and the pedants always get the final word over such obscurities
ertes 2017-02-22 02:36:11
types form a semiring under sums and products up to isomorphism, such that (->) is flipped exponentiation: a -> b ≃ b^a
maybefbi 2017-02-22 02:36:11
this is also how i became an atheist btw
merijn 2017-02-22 02:36:17
maybefbi: Welcome to the wonderful world of math ;)
maybefbi 2017-02-22 02:36:35
i.e. realizing that rules are for suckers. anything can be justified with enough arguments
ertes 2017-02-22 02:36:39
(VoidF r -> r) -- that's just isomorphic to: Void -> r
ertes 2017-02-22 02:36:43
and Void ≃ 0
ertes 2017-02-22 02:36:44
0 -> r
ertes 2017-02-22 02:36:58
0 -> r ≃ r^0
ertes 2017-02-22 02:37:08
and what's r^0? well, it's 1 =)
ertes 2017-02-22 02:37:26
and 1 is a singleton type: 1 ≃ ()
ertes 2017-02-22 02:37:47
so: VoidF r -> r ≃ 1 ≃ ()
hc_ 2017-02-22 02:38:20
Hi everyone
hc_ 2017-02-22 02:38:27
Could you have a look at this diff please: (https://github.com/VirtualForgeGmbH/hascar/commit/ee5ef2486728c5d175cfe67b942f4afd17202db2#diff-12b15ce1b1932450f4a585396dc94498)
ertes 2017-02-22 02:38:33
most of the time you can pretend that types behave like numbers, except that you don't have negatives and reciprocals =)
hc_ 2017-02-22 02:38:39
The old version compiled fine with ghc 8.0.1 but doesn't with 8.0.2
maybefbi 2017-02-22 02:38:53
ertes, that seems like a derivation out of principia mathematica
ertes 2017-02-22 02:38:59
and everything is up to isomorphism, so just write "≃" ("isomorphic to") instead of "=" (equal to)
ertes 2017-02-22 02:39:36
(and yes, i'm aware that there is a better symbol) =P
ertes 2017-02-22 02:40:14
maybefbi: type algebra is really useful for stuff like that, so i generally recommend to learn it
maybefbi 2017-02-22 02:40:29
ertes, where do i start?
ertes 2017-02-22 02:40:47
maybefbi: data ListF a x = Nil | Cons a x
ertes 2017-02-22 02:40:55
[a] ≃ Fix (ListF a)
ertes 2017-02-22 02:41:12
foldList :: (ListF a r -> r) -> Fix (ListF a) -> r
merijn 2017-02-22 02:41:16
maybefbi: Here: https://chris-taylor.github.io/blog/2013/02/10/the-algebra-of-algebraic-data-types/
ertes 2017-02-22 02:41:40
maybefbi: try to use algebraic reasoning to prove that this type is isomorphic to the more familiar: (a -> r -> r) -> r -> [a] -> r
maybefbi 2017-02-22 02:41:59
ertes, hmm ok
ertes 2017-02-22 02:42:12
you may assume the following: [a] ≃ Fix (ListF a)
ertes 2017-02-22 02:42:56
maybefbi: you should probably read merijn's link first though =)
maybefbi 2017-02-22 02:43:13
skimming it now
ertes 2017-02-22 02:43:20
don't skim it… read it
hc_ 2017-02-22 02:44:19
I've pasted the code that compiles with ghc 8.0.1 but not 8.0.2 and pointer to a url that explains what I'm missing here is appreciated: http://lpaste.net/352874
