ski 2017-02-22 06:45:16
iow, for every type `a', we're defining the type `Maybe a' as ...
ski 2017-02-22 06:45:34
(so we're defining a "family" of types, one for each concrete type we could use in place of `a')
ski 2017-02-22 06:46:09
but this (conceptual) `forall' is not the `forall' that occurs in types (`Maybe a = Nothing | Just a' is not a type, it's a `data' type specification)
ski 2017-02-22 06:46:14
similarly, in
ski 2017-02-22 06:46:21
id x = x
ski 2017-02-22 06:46:28
we can conceptually think of this defining equation as
ski 2017-02-22 06:46:34
forall x. (id x = x)
ski 2017-02-22 06:47:14
mbrock : this was going off a tangent for a bit, just to emphasize that not every `forall' one might think of would have to appear in a type
danilo2 2017-02-22 06:47:16
Hello guys! Is there any operator in Lenses that would allow me to write `[1 .. 10] & _head (fmap (+1))` ? So It will allow me to process Maybe val into Maybe val
ski 2017-02-22 06:48:10
(in the `Maybe' case, that's an example of a situation where the type variable `a' is not bound by the kind of implicitly-inserted `forall' that gets inserted just after `::' in type *signatures*)
mbrock 2017-02-22 06:48:56
basically every time we use a free type variable, there is some kind of implicit forall somewhere
ski 2017-02-22 06:49:12
well, there's some kind of implicit *binder* somewhere, yes
ski 2017-02-22 06:49:45
and, usually, it could be thought of as some kind of implicit `forall', either a type-`forall', or some other conceptual `forall'
ski 2017-02-22 06:49:54
mbrock : another thing that people sometimes stumble on : `[a] -> [a]' is *not* implicitly expanded to `forall a. [a] -> [a]'
ski 2017-02-22 06:50:12
i've been specifically talking about an implicit `forall' being inserted after the `::' in type *signatures*
ski 2017-02-22 06:51:19
if `[a] -> [a]' was implicitly expanded to `forall a. [a] -> [a]' (even if only in the case where `a' isn't mentioned elsewhere), then that would mean that `foo :: ([a] -> [a]) -> Bool' would mean `foo :: (forall a. [a] -> [a]) -> Bool' .. which is patently false
ski 2017-02-22 06:51:33
it means `foo :: forall a. ([a] -> [a]) -> Bool'
ski 2017-02-22 06:52:00
(`foo' here is just a silly example. if you like, you could think of it as being defined by `foo f = null (f [])')
ski 2017-02-22 06:53:08
mbrock : apart from `class',`instance',`data',`newtype',`type', the other situations where there's already a type variable in scope tends to involve the language extension `ScopedTypeVariables', so hopefully one knows when that is the case
ski 2017-02-22 06:53:23
going back to
ski 2017-02-22 06:53:27
length :: [a] -> Int
ski 2017-02-22 06:53:28
which means
ski 2017-02-22 06:53:32
length :: forall a. [a] -> Int
ski 2017-02-22 06:53:57
similarly to the `Maybe' case above, we can think of this as specifying
ski 2017-02-22 06:53:59
forall a.
ski 2017-02-22 06:54:05
length :: [a] -> Int
ski 2017-02-22 06:54:30
iow, for any type `a' (that the user/caller decides to pick), `length' *can* be used as having type `[a] -> Int'
ski 2017-02-22 06:54:47
mbrock : makes sense ? (any questions ?)
mbrock 2017-02-22 06:54:59
just a sec
mbrock 2017-02-22 06:56:41
right, `[a] -> [a]' isn't expanded like that in function type signatures, but all free type variables there are bound with one big forall quantifying the whole function type
ski 2017-02-22 06:57:12
yes, scoping over the whole type in the type signature, with the `forall's inserted at the front/root
contiver 2017-02-22 06:58:12
To write an SVG optimizer (along the lines of https://github.com/svg/svgo ), would it be better to write the parser from scratch, or is there an XML parser I'd benefit from using?
ski 2017-02-22 06:59:33
ok
mbrock 2017-02-22 06:59:49
and "foo :: (forall a. [a] -> [a]) -> Bool" requires a language extension, right?
ski 2017-02-22 06:59:56
yes (`Rank2Types')
ski 2017-02-22 07:00:32
so, just like something isn't a function in case its type doesn't involve `->' (specifically has an `->' as the root node in the abstract syntax tree (AST))
ski 2017-02-22 07:01:14
something isn't a polymorphic value unless its type looks like `forall a. ..a..' (for some choice of naming for the type variable `a'), where `..a..' is allowed (but not required) to refer to `a' (freely)
ski 2017-02-22 07:01:34
so, strictly speaking, `length' isn't a function, but a polymorphic value ..
ski 2017-02-22 07:02:43
.. but since the specialization from a value of type `forall a. [a] -> Int' to, e.g. `[Integer] -> Int' is implicit on the value-level, it tends to be practical to call it a "polymorphic function", or just a "function" if the polymorphic part of it isn't relevant or important at the moment
ski 2017-02-22 07:03:26
(there's no such thing as a "zero-arity function")
ski 2017-02-22 07:04:17
the important point with polymorphism is that the choice of the actual type to use in place of the type variable `a' is left to the user/caller of the polymorphic value
ski 2017-02-22 07:04:49
and so, the callee/implementor of the polymorphic value has to be prepared for *any* type the user/caller could possibly pick
ski 2017-02-22 07:05:54
in the case of constrained polymorphism, like `sort :: forall a. Ord a => [a] -> [a]', the caller will pick `a', but must also provide evidence of the constraint `Ord a', in order to be able to use `sort' as a function (passing in an argument)
mbrock 2017-02-22 07:06:10
so you wouldn't call that "foo" function a polymorphic value, but rather a function whose argument is a polymorphic value
ski 2017-02-22 07:07:03
on the flip side of the coin, `sort' itself may assume nothing about the type `a' that the caller picks, *except* that it may use the fact that `a' is known to be an instance of `Ord' (and so the methods of that class can be used to manipulate the, otherwise, opaque (to `sort') values of type `a')
ski 2017-02-22 07:07:36
mbrock : `foo :: (forall a. [a] -> [a]) -> Bool' is definitely not a type signature of a polymorphic value, right
ski 2017-02-22 07:07:51
it expects (requires !) the *argument* to be polymorphic
ski 2017-02-22 07:07:59
which is very different from itself being polymorphic
mbrock 2017-02-22 07:08:05
right
ski 2017-02-22 07:08:09
(though both things can happen at the same time ..)
Aruro 2017-02-22 07:08:33
im using System.Directory.Extra to read filesrecursively and make HTML listing with lucid. however, i get problem with unicode. Unicode characters not printed correctly. My suspicion is that Data.Text.pack does not handle FilePath unicode very well?
ski 2017-02-22 07:08:50
in the case of `foo :: (forall a. [a] -> [a]) -> Bool', `foo' *itself* will pick the type to use for `a', and the *caller* (when providing that polymorphic callback) has to be prepared for *any* such choice of `a'
ski 2017-02-22 07:09:16
in fact, `foo' may even use its polymorphic argument more than ones, using different specific types in place of `a' in each case
ski 2017-02-22 07:09:26
s/ones/once/
ski 2017-02-22 07:10:03
so, by putting `forall' in an argument types, we've flipped the roles of who picks the type, and who has to be prepared for any choice
ski 2017-02-22 07:10:09
mbrock : you see this ?
Aruro 2017-02-22 07:11:13
how do i convert file path of the form "\1045\1045..." to Text correctly? so that printed to file it was displayed correctly
mbrock 2017-02-22 07:12:15
yes, foo gets to have fun by doing e.g. ``foo f = length (f [1,2,3]) == length (f "hello")''
ski 2017-02-22 07:12:54
mbrock : so, you need `Rank2Types' to place `forall's in argument types like this
ski 2017-02-22 07:13:20
(at the "top" level of the argument types. if you need to place it in "argument types of callback arguments,&c.", then `RankNTypes')
ski 2017-02-22 07:13:36
the type `forall a. [a] -> Int' has rank one
ski 2017-02-22 07:13:51
the type `(forall a. [a] -> [a]) -> Bool' has rank two
ski 2017-02-22 07:14:20
the rank is a measure of the maximum number of `->'s one has to "dive to the left of" to reach a `forall'
mbrock 2017-02-22 07:15:17
yeah what would be a rank three type?
ski 2017-02-22 07:15:49
something like `((forall a. ..a..) -> ...) -> ...'
ski 2017-02-22 07:15:52
@type callCC
lambdabot 2017-02-22 07:15:55
MonadCont m => ((a -> m b) -> m a) -> m a
dolio 2017-02-22 07:16:11
((forall b. a -> Cont r b) -> Cont r a) -> Cont r a
ski 2017-02-22 07:16:29
callCC :: forall m. MonadCont m => ((forall b. a -> m b) -> m a) -> m a -- a sometimes proposed alternative typing, being rank-three
ski 2017-02-22 07:16:57
@type runST
lambdabot 2017-02-22 07:16:59
(forall s. ST s a) -> a
ski 2017-02-22 07:17:08
is another rank-two operation
mbrock 2017-02-22 07:17:25
okay. is there an interesting reason why Haskell has `Rank2Types' and `RankNTypes'?
ski 2017-02-22 07:17:54
(the alternative typing here would be more flexible, since `b' would be picked at each use of the "continuation", not picked at the site where it is captured)
dolio 2017-02-22 07:18:16
Way back, people were only sure implementing rank-2 was easy enough.
ski 2017-02-22 07:18:42
`Rank2Types' was implemented first. iirc, nowadays you get `RankNTypes' when you ask for `Rank2Types'
Tuplanolla 2017-02-22 07:18:59
You get a deprecation warning too.
erisco 2017-02-22 07:19:06
I hear RankNTypes is the fixed point of Rank2Types
jle` 2017-02-22 07:19:35
RankNTypes is the fixed point of Rank(+1)Types
ski 2017-02-22 07:19:39
mbrock : sometimes you want to store polymorphic things in data structures, iow have arguments of data constructors be polymorphic. that's `PolymorphicComponents'. using that, you can simulate `foo :: (forall a. [a] -> [a]) -> Bool', by inventing a new type for `forall a. [a] -> [a]', but then you get extra wrapping/unwrapping
lyxia 2017-02-22 07:20:00
Aruro: If your String is fine then Text.pack should work.
ski 2017-02-22 07:20:28
`Rank2Types' implies `PolymorphicComponents', and presumably the latter also turns on `RankNTypes' nowadays
dolio 2017-02-22 07:20:55
I don't think PolymorphicComponents turns on RankNTypes.
ski 2017-02-22 07:21:10
hm, ok
ski 2017-02-22 07:22:12
mbrock : e.g. you may have heard about how `class Eq a where (==),(/=) :: a -> a -> Bool' can be thought of as implemented in terms of `data EqDict a = MkEqDict {eq,neq :: a -> a -> Bool}', and explicitly passing dictionaries around instead of implicit type class constraints being automatically propagated (and constructed)
Aruro 2017-02-22 07:22:26
lyxia: i have cyrillic filenames, my string is obtained through getDirectoryContents (im using System.Directory.Extra)
srhb 2017-02-22 07:22:52
Is there some way to get the error in foo = bar 1 where bar = _ to actually constrain the type of bar?
mbrock 2017-02-22 07:22:59
I seem to recall that polymorphic components in data types were called "existential types" years ago
ski 2017-02-22 07:23:03
mbrock : in the case `class Functor f where fmap :: forall a b. (a -> b) -> f a -> f b', whis would be `data FunctorDict f = MkFunctorDict {fmap :: forall a b. (a -> b) -> f a -> f b}', requiring at least `PolymorphicComponents'
srhb 2017-02-22 07:23:13
Short of inlining it, of course.
ski 2017-02-22 07:23:13
mbrock : no, existentials is something different
Aruro 2017-02-22 07:23:30
lyxia : when i renderToFile in lucid i get wrong characters in these file names
Aruro 2017-02-22 07:23:59
completely unreadable
ski 2017-02-22 07:24:31
mbrock : anyway, existentials was the point i wanted to get to, next :)
mbrock 2017-02-22 07:24:41
ok :)
dolio 2017-02-22 07:25:18
srhb: -XMonoLocalBinds
ski 2017-02-22 07:25:29
mbrock : a value of type `forall a. ..a..' can be treated as a value of type `..a..', provided the user picks a particular specific type for `a'. iow for every type `a', it can be treated as having type `..a..'
ski 2017-02-22 07:26:11
mbrock : a value of type `exists a. ..a..' consists of a choice of a type `a', and a value having type `..a..'. iow, there *exists* some type `a', such that the value has type `..a..'
srhb 2017-02-22 07:26:44
dolio: Seems to do nothing.
ski 2017-02-22 07:27:01
mbrock : however, you can't (in the general case, there are some tricks that sometimes apply) recover the actual type `a' that was used when constructing the value. you have to treat it as an abstract/opaque type
Aruro 2017-02-22 07:27:15
lyxia: though less shows that characters in resulting html file are correct, like in terminal. so it seems problem of browser?
ski 2017-02-22 07:27:58
mbrock : when *consuming* a value of type `forall a. ..a..', you pick a specific type to use for `a', and then you consume the value of type `..a..', for that choice of the type `a'
srhb 2017-02-22 07:28:10
dolio: Interestingly, it works if I provoke a type error instead of using a hole.
srhb 2017-02-22 07:28:16
dolio: With and without that extension.
lyxia 2017-02-22 07:28:23
Aruro: maybe. Have you checked the encoding setting in your browser
Tuplanolla 2017-02-22 07:28:25
The browser probably assumes ISO 8859-1, Aruro.
Aruro 2017-02-22 07:28:44
lyxia: yes, i put now Unicode and all is visible correctly :)
ski 2017-02-22 07:28:48
mbrock : then *producing* a value of type `forall a. ..a..', you must be prepared for any choice that the user makes when picking `a', so you must treat `a' as abstract/opaque, being prepared for anything
ski 2017-02-22 07:29:08
mbrock : when *producing* a value of type `exists a. ..a..', you pick a specific type to use for `a', and then you produce a value of type `..a..', for that choice of the type `a'
srhb 2017-02-22 07:29:10
I guess I'll just make a data constructor that will always be an error.
ski 2017-02-22 07:29:29
mbrock : then *consuming* a value of type `exists a. ..a..', you must be prepared for any choice that the producer/implementor made when picking `a', so you must treat `a' as abstract/opaque, being prepared for anything
Aruro 2017-02-22 07:30:37
lyxia: ty
ski 2017-02-22 07:30:42
mbrock : so in this sense, `forall' and `exists' are exactly the opposites of each other, exchanging the roles of producers and consumers, wrt who gets to pick the type, and who must be prepared for any choice of the type
ski 2017-02-22 07:30:58
mbrock : here's a silly example of `exists' :
ski 2017-02-22 07:30:58
frob :: Bool -> exists a. (a,a -> a,a -> String)
ski 2017-02-22 07:31:12
frob False = ( True ,not,show)
ski 2017-02-22 07:31:29
frob True = ("False",reverse,id)
ski 2017-02-22 07:32:10
mbrock : you should note that the choice of the type `a' in the return type of `frob' here depends on the *run-time* input value
ski 2017-02-22 07:32:18
mbrock : makes sense, so far ?
mbrock 2017-02-22 07:34:10
is your type signature a typo for ``Bool -> exists a. (a, a -> a, String)''?
mbrock 2017-02-22 07:34:28
wait nevermind
ski 2017-02-22 07:34:30
no
mbrock 2017-02-22 07:34:46
sorry I was just confused by your spacing and the precedences of , and -> :)
ski 2017-02-22 07:35:04
in the `False' case, `a = Bool', and so `show :: Bool -> String' fits in the third component
mbrock 2017-02-22 07:35:18
yes, my bad. Is that code valid GHC with some extension?
ski 2017-02-22 07:35:22
in the `True' case, `a = String', and so `id :: String -> String' fits in the third component
ski 2017-02-22 07:35:26
no
ski 2017-02-22 07:35:50
i'm using the `exists' notation to get the concept across (imho) more clearly
ski 2017-02-22 07:36:13
iirc, in LHC, you could actually use `exists' .. but only in argument types
ski 2017-02-22 07:36:28
in GHC, there's basically two ways to *encode* an `exists'
mbrock 2017-02-22 07:36:33
ok
ski 2017-02-22 07:36:43
(if you have time, i'll go through both of them)
ski 2017-02-22 07:37:06
but i hope the basic idea of how `exists' is supposed to work is sufficiently clear
ski 2017-02-22 07:37:44
(Mercury is a language that allows existential quantifiers in types, called `some' there)
ski 2017-02-22 07:38:56
mbrock : anyway, to use a value of type `(a,a -> a,a -> String)', basically what you can do is pass the `a' value through the function of type `a -> a' some fixed number of times, and then convert it to a `String' to inspect the result
ski 2017-02-22 07:39:11
er, of type `exists a. (a,a -> a,a -> String)', i meant
mbrock 2017-02-22 07:40:21
yeah
ski 2017-02-22 07:40:34
mbrock : this is related to abstract data types. one way to specify the *interface* of e.g. queues, would be to have a type `exists q. (q,a -> q -> q,q -> Maybe (q,a))', where the first component is the empty queue, the second is the `enqueue' operation, the third is the `dequeue' operation
ski 2017-02-22 07:41:11
each *value* of type `exists q. (q,a -> q -> q,q -> Maybe (q,a))' would correspond to a (potentially) *different* implementation of the queue interface
ski 2017-02-22 07:41:43
you'd use such an implementation by "opening" it once, then operating with the operations inside until you're done with your queue
ski 2017-02-22 07:42:52
one choice would be to pick `q' as `[a]'. a more efficient choice would be to pick it as `([a],[a])', where we represent a queue with elements like e.g. `2',`3',`5',`7',`11',`13' as `([2,3],[13,11,7,5])'
ski 2017-02-22 07:43:14
iow `front ++ back' is conceptually represented as `(front,reverse back)'
ski 2017-02-22 07:44:08
mbrock : anyway, now i want you to realize that the type `(exists a. ..a..) -> ...' is basically the same thing as `forall a. (..a.. -> ...)' (brackets for emphasis)
ski 2017-02-22 07:44:11
iow
ski 2017-02-22 07:44:20
length :: forall a. ([a] -> Int)
ski 2017-02-22 07:44:22
is the same thing as
ski 2017-02-22 07:44:30
length :: (exists a. [a]) -> Int
ski 2017-02-22 07:44:54
in the former case, we say that for any type `a', `length' can be applied to a value of type `[a]', yielding a result of type `Int'
dolio 2017-02-22 07:44:59
srhb: Hmm, strange.
