3 ms·

So `A` is a type, and `Type` is a type?

• throwaway17_17 7y ago
  In this context, ‘A’ is an instance of Type, and ‘Type’ is the type of types (usually the term used for type of type is Kind). So while ‘x’ could be the value 7 and ‘A’ could be the type Int, the ‘B(x):Type’ means that the value of B(x) is some Type, could be Int, Char, Bool, etc.
  • mcphage 7y ago
    Thank you!
• curryhoward 7y ago
  `A` is a type, yes. Whether `Type` is a type depends on what type system you're working in. If `Type` is its own type, then it turns out you can use that to do infinite recursion (this is called Girard's paradox). Dependent types are often used for proving theorems, where infinite recursion corresponds to circular reasoning—a big no-no. So, in many dependently typed languages, `Type` is not its own type (instead, it's common to have an infinite tower of types: `42` has type `Int`, `Int` has type `Type0`, `Type0` has type `Type1`, `Type1` has type `Type2`, and so on). However, if the programming language is just used for programming and not for proving, then it's perfectly fine (and quite convenient) to have `Type` be its own type.