[Haskell-cafe] ghci's choice of names for type variables
Julian Bradfield
jcb at inf.ed.ac.uk
Sat Oct 30 11:06:35 UTC 2021
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.
More information about the Haskell-Cafe
mailing list