How to disable Kind annotations in REPL

Help
#1

Hello :slight_smile:

There is a kind annotation now

> f x = x 
> :type f
forall (t1 :: Type). t1 -> t1

> :type map
forall (f :: Type -> Type) (a :: Type) (b :: Type). Functor f => (a -> b) -> f a -> f b

I am a newbie (with a beginner perspective aiming at programming real world programs) and I find it excessively leaned over, ML theory for compiler writers, and also overly pedantic. F#, OCaml don’t show this information and I guess they had plenty of time to implement such things.

How will this be of use to me ? Can a practical (stuff like halogen) programmer quantify when will I require this information ? Isn’t it purely for display ? I thought this was for the likes of Proofs Assistants.

This led me to ponder the when : Information dump should be contextual.

I wish I could turn off this extra typing of types, because I will probably never ever have to use it or I could do without. I don’t know what fields of programming it helps.

A toggle to switch On and Off kind annotation would reduce scattering of relevant type output that I keep on laboriously sieving to pick them up, while filtering the kind typing noise/bloat. It would revert outputs to single lines when possible and be a lighter read again. I have limited register capacity in my head ! This makes me undo mentally this feature all the time.

A toggle lets switch according to the highness of code. It could be “:type” and “:kind” (fullest).

I checked out a version of purescript anterior to this hard modification for development. I will pull out the latest version for production. Will I be missing any new language features or hit deprecated ones ?

#2

TLDR: F# and OCaml don’t have higher-kinded types, i.e. the capability to have a function parameterized over a type that takes other types, so there is no way that information would ever be useful to you. While 'a list, a list of any type a is valid, 'a 'f is not, i.e. any type f that itself takes type a.

The rest of this post deals with why we might want to care about this information so if that is truly secondary to “Why was it put in the REPL and how do I disable it?” let it be noted that none of that is answered below.

A higher-kinded type can be expressed almost like a function in the type system, hence this f :: Type -> Type notation that is used. What you get when you apply a type to this is a new type, which is exactly the same thing we do with functions; we call them with values to get new values.

> :kind Array
Type -> Type

Array would be a valid stand-in for f here because it takes a type to produce a concrete type:

> :kind Array Int
Type

When we apply a type here we get the concrete type we were expecting: Array Int has the kind Type.

We can follow the same procedure with more type parameters as we see here with Map (data Map k v):

> :kind Map
Type -> Type -> Type

Map would not be a valid stand-in for f because it takes two type parameters to produce a concrete type.

> :kind Map String
Type -> Type

Map String, meaning any map keyed by Strings would be a valid stand-in, because it takes one type parameter to produce a type.

> :kind Map String Int
Type

Once we apply two type parameters we are finally down to a concrete type.

The role of the kind part in the type signature you’ve posted is that it allows you to talk about a general shape of a structure’s role in the type signature. Without noting this information or allowing it to be expressed in the type we’d have to settle for having functions either by passing interfaces to functions to generate functions, i.e. basically functors as they look in OCaml, which is a much more tedious version or some other version that is not as convenient as higher-kinded types + type classes.

Edit:

Since you said you are new and there is a good chance you are trying to find your way around generics in general considering the question, I think reading something like this chapter might be useful. There are a couple of Haskell-isms in there but the concept is exactly the same in PureScript and I haven’t found anything written for PureScript that I think would be a better intro. I will be rewriting these materials into PureScript some time in the near future, so this is the best I have for now.

1 Like
#3

Just curious. Have you read through any of the materials in my learning repo? If so, would you still say “I haven’t found anything written for PureScript that I think would be a better intro”?

1 Like
#4

I found several places where this showed up in your reference (which I think is fantastic, by the way, but very extensive and not at all the same nature as the materials I linked). The one that I like most from what I found is this one: Explaining Kinds - PureScript: Jordan's Reference

It’s probably not correct to say I don’t think it’s as good an intro, because I think it explains what I would want to have explained about kinds, but it’s divorced from the context where it’s most applicable. What I like about the material I linked (which, full disclosure, I wrote) is that it’s explained in the exact context where it comes up. It’s a brief interlude that we cover so that we can explain how it fits together to build the containerLength function, so we get the surrounding purpose and context very easily from it. The downside to this is that it’s not a very good reference for the topic; it’s best read with the surrounding parts.

Our Haskell materials couldn’t be written as a reference (which is what you’ve done very well) because they’re meant to take someone who hasn’t written any Haskell or maybe covered at most the first part of chapter one (functions, how to write and use them) and enable them to internalize a pattern for writing production Haskell applications. I meant no offense or even to pass judgment on your reference.

2 Likes
#5

That depends on how ‘anterior’ the version you’re using is. If you’re developing with an 0.14 series compiler but intend to release with a 0.15 series compiler, your difficulties will include, at a minimum, that any FFI you do is going to need some (minor, automatable, but not optional) rewriting and any libraries you use that use FFI are going to need to have different versions in development and production. If you’re developing with an 0.13 series compiler (which I suspect is how far back you’d have to go to revert this change), or goodness forbid even earlier, you’re going to have a Bad Time. I don’t recommend this approach in either case.

1 Like
#6

I definitely see the value in that approach. It does a really good job of answering questions that naturally arise as I read through the post. The context you provide makes a big difference!

#7

You are really a wise man, I love how you handle this !

You have the soul of a teacher :slight_smile:

Thx for the pedagogical reference and guidance.

#8

I really hope it helps. It can be really hard to learn these things. If you have any feedback, feel free to contact me either via the e-mail in the README of that repo or in the repo. I’m working on the PureScript version over at GitHub - quanterall/PureScriptMaterials: Materials for learning PureScript but it’ll be a while before they’re representative of what we’d want for PureScript (both in use cases and accurate adaptation).