Type level computation materials

Dialog.md

vyorkin Is there any tutorial / blog post explaining the basics of type-level ? I mean RowCons and things in typelevel-prelude. I’m reading https://liamgoodacre.github.io/purescript/2017/05/27/row-lacks.html and I think I’ve got the basic idea of how it works, but I can’t understand the implementation. This is a quick post about the new RowLacks type class that was added to purescript-typelevel-prelude. This can be used to require that a row does not contai...  vyorkin For example its hard for me to understand what is going on here: https://github.com/purescript/purescript-typelevel-prelude/blob/master/src/Type/Data/Boolean.purs#L40

-- | And two `Boolean` types together
class And (lhs :: Boolean)
          (rhs :: Boolean)
          (output :: Boolean) |
          lhs -> rhs output
instance andTrue :: And True rhs rhs
instance andFalse :: And False rhs False

and :: forall l r o. And l r o => BProxy l -> BProxy r -> BProxy o
and _ _ = BProxy

I only know about row polymorphism / row types, kinds, symbols & SProxy, need some entry-level readings (edited)   justinw do you know what fundeps do? https://leanpub.com/purescript/read#leanpub-auto-functional-dependencies

vyorkin @justinw I don’t think I understand them, re-reading this

• reading again https://github.com/paf31/24-days-of-purescript-2016/blob/master/10.markdown be back soon

paluh @vyorkin I'm considering this article (no worries it is not "a paper") http://www.cse.chalmers.se/~hallgren/Papers/hallgren.pdf ("Fun with Funtional Dependenies") as a really great introduction which should explain this And type class 😉 (edited)

justinw that's some suspicious not-paper

vyorkin haha, thanks! I’ve re-read the section about fun deps in PS book, think I understand the purpose of them now so when we have a multiparameter type class like this in the example from the book

class Stream stream element where
  uncons :: stream -> Maybe { head :: element, tail :: stream }

and this function

genericTail xs = map _.tail (uncons xs)

we need to help compiler to infer the right type by saying that “there is a function from stream types to (unique) element types” stream -> element which will be String -> Char for our function going to read this not-paper paper now 🙂 (just kidding, it looks simple, I believe I have a chance of understanding smth) (edited)

paluh @vyorkin I've found (I'm not sure if it is the simplest approach) that simple method which is a Proxy allows me to force type level computation in PureScript: http://try.purescript.org/?gist=cef92915b6348b18149a5dc347b36e26 

thomashoneyman @vyorkin I’m new to this as well and I need to do some reading. Glad to see these resources posted!

paluh There is also additional important thing regarding overlapping instances in PureScript which is somewhat related to the topic. If you want to force resolution order of instances you have to name them in alphabetical order - example: http://try.purescript.org/?gist=0fe374822218f93aabbfe2f197eca402 (edited)

I'm not sure if I understand docs correctly but they seem to be wrong (third paragraph of the first section): https://github.com/purescript/documentation/blob/master/language/Type-Classes.md

goodacre.liam yeah it's currently alphabetical, however they will be an error in the next release: 0.12