Assorted reactions I had while reading "Simply Easy! An Implementation
of a Dependently Typed Lambda Calculus" paper. (I wonder where to send
this message).
pi replaces Fun (type of function), lam stays lam (value of function).
It took me a while to figure out that that was what was going on... it
was not stated explicitly, and the relative appearances of the three
things (forall, fun and lam) did not at all clarify things (neither the
mathematical symbol forms, nor what the implementation called them). It
would be simpler though more tedious to merge values and types first (it
was said to simplify some aspects of the code after all), without
changing fun to pi
(aka becoming dependent - it's just one in which the range, instead of
sitting there on the right of the arrow, may [depend on / vary with] the
value applied to the lam being typed -- you cannot know a concrete type
of the result (the range) until you know the concrete type and then the
concrete value of the argument. Just like allowing parametric
polymorphism in Haskell: (id :: a -> a), meaning that you can only know
that the result is Bool once you know that the argument is of type bool.
The only difference with dependent types being, you also may have to
know whether the argument is True or False (which is equally well
unknown to a seperate-compilation compiler, in most cases, as the
argument's concrete type is). Combined with unifying types and values,
this means polymorphism is easy (with some explicitness... extra lams to
capture the types that may vary, even if they are not used to compute
the value of the result). I then wonder how this type system is used
like rank-2 and weirder... ok.
haskell: runST :: forall a. (forall s. ST s a) -> a
lp:
runST :: forall a::*. (forall s::*. ST s a) -> a
or
runST :: forall a::*. forall x::(forall s::*. ST s a). a
easy!!!! the "->" in the type is nothing to do with lam, merely
equivalent to fun, just a syntax sugar that's immediately turned into
forall(pi). The rank-2 argument, in lp, takes an 's' argument that it
needs to use to create any internal ST parts according to their 's'
arguments. runST invents one, and e.g. newSTRef or readSTRef consumes
one, as they are primitives (unless there is another sound way to
implement them).
and we all know typeclasses are really weird and troublesome sugar...
and the dictionary approach is "easy" to do explicitly here..?
natElim's type explains much more to me what it does than foldNat's type
does!
I would have preferred figures 15 and 16 to have bluish backgrounds, as
they are added stuff and they don't stand on their own (but... are
unnecessary to fundamental dependent types... but some of the other
Nat-stuff _is_ blue)
Where is the .lhs source of the paper itself, to see how it was done?
Probably the "uniplate" library could simplify it somewhat for those who
know uniplate already.
It is quite right about (type) inference - it seems some of the most
important research for dependently typed languages is actually being
done by GHC, in implementing type inferences that have to be predictable
and powerful (and work with a fairly sophisticated type system...). It
is the reason that I can't easily write a dynamically-typed Haskell
interpreter that doesn't do type inference - class instance selection is
quite hard, especially in the presence of defaulting, `seq`, complicated
type-restricting signatures, and
functional-dependencies/associated-types. (I thought it might be
interesting to have a way to try to produce _examples_ of
type-incorrectness for when a type error message is incomprehensible.
Of course some programs are NOT dynamically type-incorrect and it
wouldn't be able to find an example in those, and it might be unsafe in
other ways like if it can't enforce runST's rank-2 type signature when
the result is demanded)
Isaac
