Statically safe dynamic typing à la Python

Hi, Habr.

The other day in one of my hobby project, the task arose of writing a repository of metrics.

The task itself is solved very simply, but my problem with Haskel (especially in projects for my own entertainment) is that it is impossible to simply take and solve the problem. It is necessary to decide, expand, abstract, abstract and then further expand. Therefore, I wanted to make the storage of metrics extensible so as not to specify in advance what they will be there. In itself, this is a topic for a separate article, and today we will look at one small ingredient: writing a type-safe wrapper for unknown types in advance. Something like dynamic typing, but with static guarantees that we won’t do nonsense.

The article, I think, will not reveal anything new for experienced Haskelists, but now at least we will put this ingredient right away and will not be distracted by it in subsequent articles. Well, or you can not be so modest and say that I have already invented a whole design pattern.

So, first we formulate the problem. We need to be able to associate any objects with values ​​of previously unknown types. Or, in other words, it is necessary that the values ​​of previously unknown types act as keys in some map.

Naturally, we are not mad and we will not demand the support of values ​​of absolutely any type. We require that the type (even if unknown) support comparison in the sense of ordering. In terms of Haskel, this means that we support such types a , which implement the Ord a class.

Note that we could demand support for taking a hash and checking for equality, but for several reasons, it will be more convenient and clearer to limit ourselves to comparison.

When it comes to storing values ​​about which it is known that they implement a certain time class, existential types are usually used in Haskel:

 data SomeOrd where MkSomeOrd :: Ord a => a -> SomeOrd 

So, if we are given an object of type SomeOrd and we did pattern matching on it:

 foo :: SomeOrd -> Bar foo (MkSomeOrd val) = ... (1) ... 

then at point (1) we don’t know what type val has, but we know (and, most importantly, the type checker also knows) that val implements the Ord class.

However, if the function of the type class implies two (or more) arguments, then there is little use for such a record:

 tryCompare :: SomeOrd -> SomeOrd -> Bool tryCompare (MkSomeOrd val1) (MkSomeOrd val2) = ? 

To use the Ord methods, it is necessary that both val and val2 the same type, but this is absolutely not necessary! So, our SomeOrd useless. What to do?

In spite of the fact that Haskel is a compiled language with aggressive type erasure (after compilation there are generally none), the compiler can still generate type runtime if asked for it. The role of the representative of type a is the value of type TypeRep a , and a request The typeable responds to the Typeable .

In addition, if we have two different instances of rep1 :: TypeRep a, rep2 :: TypeRep b , then we can compare them and check whether they represent the same type or not. Moreover, if they actually represent the same type, then, obviously, a coincides with b . And, most importantly, the function of checking the representations of types for equality returns a result that can convince the type taker of this:

 eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b) 

What kind of nonsense is this?

First, eqTypeRep is a function.

Secondly, it is polymorphic, but not only by type, but also by the varieties of these types. This is indicated by the part forall k1 k2 (a :: k1) (b :: k2) - this means that a and b can be not only ordinary types like Int or [String] , but also, for example, zapromouchennymi designers (see DataKinds and other attempts to make Haskel seized). But we do not need all this.

Third, it takes two runtime views of potentially different types, TypeRep a and TypeRep b .

Fourth, it returns a value of type Maybe (a :~~: b) . Here is the most interesting.

If the types do not match, then the function returns a normal Nothing , and everything is in order. If the types are the same, the function returns Just val , where val is of the type a :~~: b . Let's see what this type is:

 -- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is -- inhabited by a terminating value if and only if @a@ is the same type as @b@. -- -- @since 4.10.0.0 data (a :: k1) :~~: (b :: k2) where HRefl :: a :~~: a 

Now let's reason. Suppose we get a val value of type a :~~: b . How could it be built? The only way is with the help of the HRefl constructor, and this constructor requires that on both sides of the icon :~~: stand for the same thing. Therefore, a coincides with b . Moreover, if we zapattern match on val , then the tick checker will also know about it. Therefore, yes, the eqTypeRep function returns proof that two potentially different types are the same if they are actually equal.

However, in the paragraph above, I lied. No one bothers us to write something like

 wrong :: Int :~~: String wrong = wrong --    

or

 wrong :: Int :~~: String wrong = undefined 

or break the system in a bunch of slightly less obvious ways. This is one of the manifestations of the well-known in narrow circles of the statement that Haskel is inconsistent as logic. In languages ​​with stronger type systems, such definitions are not invoked.

That is why in the piece of documentation cited just above, the terminating value is mentioned. Both variants of the implementation of wrong above do not produce this same terminating value, which returns us a bit of reason and confidence: if our program has finished on Haskell (and did not encounter undefined ), then its result corresponds to the written types. Here, however, there are some details related to laziness, but we will not open this topic.

And, by the way, the second manifestation of the weakness of Haskel in the code above is the type of the function eqTypeRep . In stronger languages, it would return a value of a stronger type, which would not only prove the equality of types, if they are in fact equal, but also give evidence of their inequality , if they are in fact unequal. The inconsistency of Haskel logic, however, makes such functions a bit meaningless: it is all important when you use the language as a prover theorem, and not as a programming language, but haskel as a prover is not particularly used.

Well, okay, enough of the matrix and type theory, back to our metrics. Now just draw an owl. The discussion above hints that it is enough to keep in our existential type also this most runtime representation of the type, and everything will be fine.

This leads us to the next implementation of our wrapper type:

 data Dyn where Dyn :: Ord a => TypeRep a -> a -> Dyn toDyn :: (Typeable a, Ord a) => a -> Dyn toDyn val = Dyn (typeOf val) val 

Now we write a function that accepts the following:

1. two values ​​of type Dyn ;
2. a function that produces something for two values ​​of any type ,
   
   based only on the constraints mentioned when creating Dyn ( forall is responsible for this),
   
   and which is called if both Dyn store values ​​of the same type;
3. and the fallback function, which is called instead of the previous one, if the types are different:

 withDyns :: (forall a. Ord a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn -> Dyn -> b withDyns f def (Dyn ty1 v1) (Dyn ty2 v2) = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2 

SomeTypeRep is an existential wrapper over TypeRep a for any a .

Now we can implement, for example, a test for equality and comparison:

 instance Eq Dyn where (==) = withDyns (==) (\_ _ -> False) instance Ord Dyn where compare = withDyns compare compare 

Here we used the fact that SomeTypeRep can be compared with each other, so the fallback function for ordering is also compare .

Is done.

Only now it’s a sin not to generalize: note that inside Dyn , toDyn , withDyns we don’t use Ord specifically, and it could be any other set of constraints, so we can enable the ConstraintKinds extension and generalize by parameterizing Dyn specific set of constraints that needed in our particular task:

 data Dyn ctx where Dyn :: ctx a => TypeRep a -> a -> Dyn ctx toDyn :: (Typeable a, ctx a) => a -> Dyn ctx toDyn val = Dyn (typeOf val) val withDyns :: (forall a. ctx a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn ctx -> Dyn ctx -> b withDyns (Dyn ty1 v1) (Dyn ty2 v2) f def = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2 

Then Dyn Ord will be our desired type, and, say, Dyn Monoid will allow you to store arbitrary monoids and do something monoidal with them.

Let's write the instances we need for our new Dyn :

 instance Eq (Dyn Eq) where (==) = withDyns (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns compare compare 

... only it does not work. Typchecker doesn't know that Dyn Ord also implements Eq ,

so you have to copy the entire hierarchy:

 instance Eq (Dyn Eq) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Eq (Dyn Ord) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns d1 d2 compare compare 

Well, now everything is exactly.

... unless, in modern haskel it is possible to make so that taypcheker himself would display instances of a type

 instance C_i (Dyn (C_1, ... C_n)) where ... 

for there comes out something prologonlike, but I haven’t done it yet, I’ll have to sit around. Stay tuned.

And also, if you carefully squint, you will notice that our Dyn suspiciously similar to a dependent pair of the form (ty : Type ** val : ty) from over-the-top languages. But only in languages ​​known to me it is impossible to match the type, for parametricity (which in this case, IMHO, is interpreted too widely), and here it seems that it is possible.

But the most important thing is that now you can safely have something like Map (Dyn Ord) SomeValue and use any values ​​as keys, as long as they support the comparison. For example, identifiers with the description of metrics can be used as keys, but this is a topic for the next article.