Leon Smith <[EMAIL PROTECTED]> wrote (about a week ago):
> [...]
> With dependent types, would it be possible to get types from values (i.e.
> types that you haven't actually declared before.) One example would be the
> group of integers modulo n. It sounds to me like types would then be first
> class. So, concieveably, I could write a function Z : Integer -> Type,
> where Z n would be the group of integers modulo n.
The question is very important.
Even if the dependent (or maybe, dynamic) types do *not* allow this,
still,
in what way the language could support the dynamic domains ?
The matter is that the recent Haskell type system relevance to
mathematics is, boldly speaking, as follows:
Mathematics \ Haskell = Dynamic domains
The word `domains' is set cautiously: i do not know what are the
dependent types, neither the dynamic types - also mentioned in the
recent discussion of February 1999.
Also, some implementations provide certain library for dynamic
operations with type descriptions.
Has this anything to do with the above question?
You see, it is often needed to change dynamically the computation
domain. For example, many algorithms require computation in
Z/(m) - integer modulo m - for m = m1,m2,... with the set of m(i)
statically not known. The domains Z/(m(i)) have different
properties and even have to be supplied with the different sets of
instances. The same is with Vector of dynamically defined dimension.
As to the programming, i mean something like this:
data Res &a a = Res' &a a
--
-- `a' is usual parameter: ranges over types;
-- &a is the value parameter: ranges over `a'.
-- Res &a === <Res &a>
-- is understood as the type constructor (data type) evaluated
-- dynamically from the parameter value: dynamically varying
-- type constructor.
The instances for <Res &a> are defined dependently on &a.
Furthermore, an instance may be defined or not at all, depending on
the value of &a.
Thus, <Res 3> needs the Field instance, <Res 4> does not.
And does <Res (f 2)> need the Field instance?
Well, f 2 evaluates at the run-time, and then it becomes known,
whether, say,
inv :: Res (f 2) Z -> Res (f 2) Z
(of class Field) is correct.
The run-time overhead of this depends on how the programmer organizes
the type.
For example, Field <Res &m>, &m :: Z,
is correct when &m > 1 && isPrime &m
So, if we declare
data Res &a a = Res' (&a,Factorization a) a
the check for Field (Res &n), &n :: Z,
would only require to peer into the Factorization part of the data.
And this part is computed once - the programmer setting (factor &a)
somewhere - further checks use the ready value.
And maybe, the memoisation can be applied for the type evaluation.
Further illustration:
type Z = Integer
f :: Z -> (Z5, Z5, Z8, Zn3)
f n =
let
Z4 = Res 4 :: Res &Z Z -- residue domain modulo 4 - Z/(4)
Zn2 = Res (n^2) -- ... Z/(n^2)
Z5 = Res 5
r1 = Z5 3 -- element of Z/(5)
r2 = Z4 1 -- ... Z/(4)
r3 = Zn2 1 -- ... Z/(n^2)
in
(r1+r1, inv r1, r2+r3)
Then f 2 --> (Z5 1, Z5 2, Z4 2) (3+3 = 1 (mod 5) ...)
Here r2+r3 works because the domains <Res 4> and <Res (2^2)> become
equal. Also the domains and instances for r1+r1, inv r1
are solved statically, because the parameter value &n = 5 is known
at compile-time. The domains for r2+r3 are solved partially at
run-time. Further,
f 3 --> error ... "r2+r3, r2 :: <Res 4>, r3 :: <Res 8>"
"mixing values from different domains"
Setting in this program `inv r2' after r2 = ... yields
error "inv r2: no Field instance for <Res 4>"
This is detected at the stage of compilation, because &m = 4 is
known statically (and assume here, its primality too).
Further, adding `inv r3' to result gives
f 1 --> ... inv (<Res 2^1> 1) ... -> <Res 2> 1
- matches Field instance.
f 2 --> ... inv (<Res 2^2> 1) ... ->
error "inv r3: no Field instance for <Res 4>"
The programmer should also have a tool to specify how eagerly the
dynamic domains have to be checked.
Is this correct to think of such features - remaining in the area of
the "typeful" functional programming?
------------------
Sergey Mechveliani
[EMAIL PROTECTED]
