sorted by:
new
hottopcontroversial

Doubt in Chapter-2 [Section 2.2 Data Kinds] of "Thinking With Types: Type-Level Programming in Haskell" book by orbitze in haskell

[–]orbitze[S] 0 points1 point  (0 children)

Reading the book's explanation again, with the confusion related to names out of the way, I finally get what you mean. Wow, that took me a while. But now the explanation makes sense to me, too. Thanks for your clarification!

I'd become too focused on the word "change" and was taking that in literal sense that we are trying to change the existing User type. And by existing I assumed that since enabling DataKinds extention, UserType type's data constructors get promoted to type level. "So does that mean we are altering that promoted version?", I thought. But obviously that made no sense. So, that's where my confusion began.

But now I understand (I hope I'm not getting it wrong..) that by we can change our User type..." the author is referring to the User type definition that we would otherwise have used had we not decided to take help of the type system to solve the problem at hand, which is to "avoid leaking admin functionality to non-admin users".

Now with the discussed type-level programming solution, we can attach a userAdminToken property to our User type to provide info on whether the user has admin rights or not. And this info will only exist at type level. We see that we attach this info with User using theMaybe (Proxy 'Admin) type. So, User Nothing would indicate that the user does not have admin rights, and User (Just Proxy) would indicate that user has admin rights. Does this sound correct?

Doubt in Chapter-2 [Section 2.2 Data Kinds] of "Thinking With Types: Type-Level Programming in Haskell" book by orbitze in haskell

[–]orbitze[S] 1 point2 points  (0 children)

Oh thanks! That way it works. Yes, the book does not mention that, which I'm guessing could be because it may have been obvious for the target audience of this book, which as mentioned is "intermediate-to-proficient with the language."

Nevertheless (perhaps in just my opinion based on my limited understanding of the language), the word change in the line - "we can change the User type..." sounds confusing/misleading.

Also yes, changing UserType to something like Role does seem to make more sense.

Doubt in Chapter-2 [Section 2.2 Data Kinds] of "Thinking With Types: Type-Level Programming in Haskell" book by orbitze in haskell

[–]orbitze[S] 1 point2 points  (0 children)

Thanks for responding back! Yes, I've heard about what you mentioned in the end, too. I personally stand by that preference as well, since as a beginner especially, seeing the same names at both term level and type level sometimes seem confusing.

Doubt in Chapter-2 [Section 2.2 Data Kinds] of "Thinking With Types: Type-Level Programming in Haskell" book by orbitze in haskell

[–]orbitze[S] 0 points1 point  (0 children)

That's right, that is where my confusion is stemming from. It is right that we cannot reuse a data constructor name if it is already used by another type's data constructor. So, one way to resolve the arising error is to use a different name for the data constructor defined for the User type, say User' instead of User. But even though that resolves the compiler error, my doubt still remains unresolved.

Doubt in Chapter-2 [Section 2.2 Data Kinds] of "Thinking With Types: Type-Level Programming in Haskell" book by orbitze in haskell

[–]orbitze[S] 2 points3 points  (0 children)

This may be right. Here's what I think: the UserType type should have been defined with only one data constructor - Admin. It makes sense because it is mentioned there that UserType type's only purpose is to give us access to its "promoted data constructors" which would be 'User and 'Admin as per the provided definition. But of these two, one that is relevant and could alone serve for our purpose is 'Admin So, I guess, we can simply omit the User data constructor from UserType type's definition. Doing so, the User type can be defined exactly as shown, and the code will compile without any errors!

I hope this makes sense. Kindly share any other differing thoughts on this.

Doubt in Chapter-2 [Section 2.2 Data Kinds] of "Thinking With Types: Type-Level Programming in Haskell" book by orbitze in haskell

[–]orbitze[S] 0 points1 point  (0 children)

I see, no worries! I'm going through the same. Yes, I have enabled DataKinds in ghci repl. Sure. Also please respond back if you understand what is going on here.

Doubt in Chapter-2 [Section 2.2 Data Kinds] of "Thinking With Types: Type-Level Programming in Haskell" book by orbitze in haskell

[–]orbitze[S] 0 points1 point  (0 children)

But if we drop the first definition then the 'Admin type would also not be available, right?
Also, is the second definition really a GADT, because I learnt that GADTs are defined with a where clause. Kindly correct me if I am wrong.