[Haskell-cafe] ghci's choice of names for type variables

[Richard Eisenberg]

Joachim is right that, when you use a function that's already defined somewhere, GHC will use its choice of type variable names. That explains all the 'a's you observe. As for the others, `t` is GHC's letter of choice most of the time, and it's hard to predict (even for me, with pretty deep knowledge of the type checker) when it will use `p`.

Bottom line: don't think about this too much -- there's not much of a signal in the noise. :)

Richard

> On Oct 30, 2021, at 7:06 AM, Julian Bradfield <jcb at inf.ed.ac.uk> wrote:
> 
> I have tried to answer this by google and the list archives, but
> without success, though it wouldn't surprise me if there is a post
> buried somewhere.
> 
> This is GHCI 8.10.7.
> 
> When ghci infers types, it sometimes produces types with "a", with
> "t", and with "p" (and maybe others), as in the following set of
> examples:
> 
> Prelude> h (x : xs) = x
> Prelude> :t h
> h :: [a] -> a
> Prelude> foo f x = not(f x)
> Prelude> :t foo
> foo :: (t -> Bool) -> t -> Bool
> Prelude> bar f x = (f x) + 1
> Prelude> :t bar
> bar :: Num a => (t -> a) -> t -> a
> Prelude> barb f x g y = (f x)+(g y)
> Prelude> :t barb
> barb :: Num a => (t1 -> a) -> t1 -> (t2 -> a) -> t2 -> a
> Prelude> gar f x = f x
> Prelude> :t gar
> gar :: (t1 -> t2) -> t1 -> t2
> Prelude> fooa x = x
> Prelude> :t fooa
> fooa :: p -> p
> 
> What is its rationale? I have attempted to find it in the typechecker
> code, and I see things that suggest "t" is something to do with tau
> types (monotypes?), and "p" has something to do with levels, but going
> from basic Haskell and a modest theoretical acquaintance with System F to
> being able to read the GHCi type-checker is several steps too far!
> 
> Can somebody give me a brief explanation of what's going on? In
> particular, is there actual information about the types in the choice
> of letters, or is it just incidental information about the way type
> inference proceeded?
> 
> Thanks,
> Julian.
> 
> -- 
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> 
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.