Statically secure dynamic typing à la Python

Hi, Habr.

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

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

The article, I think, will not open anything new for experienced Haskellists, but now we will at least put this ingredient out of the box and will not be distracted by it in subsequent articles. Well, or you can be not so modest and say that I already came up with a whole design pattern.

So, first we formulate the problem. We need to be able to associate some 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 kind of map.

Naturally, we are not insane and we will not require the support of values ​​of any type. We require that the type (even if unknown) support comparison in the sense of ordering. In terms of Haskell, this means that we support types athat implement a timeclass Ord a.

Note that we could demand support for taking a hash and checking for equality, but for a number of reasons it would be more convenient and clear to limit ourselves to comparison.

When it comes to storing values ​​that are known to implement some type of class, existential types are usually used in the Haskell:

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

So, if we are given an object of type SomeOrdand we made pattern matching on it:

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

then at the point (1)we don’t know what type exactly has it val, but we know (and, most importantly, the typsekher also knows) what valimplements the typclass Ord.

However, if the type functions of the class imply two (or more) arguments, then the use of such a record is not enough:

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

To apply the methods, Ordit is necessary that and val, and val2have the same type, but this is absolutely not required to be performed! It turns out that ours is SomeOrduseless. What to do?

Despite the fact that the Haskell is a compiled language with aggressive type erasure (after compilation, they aren’t there in general), the compiler can still generate runtime type representatives if asked about it. The role representative of the type ais the value of the type TypeRep a, andrequestgeneration is answered by a class Typeable.

In addition, if we have two different instances 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, acoincides with b. And, most importantly, the function of checking type representations for equality returns a result that can convince the typcher of this:

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

What nonsense is written here?

Firstly, eqTypeRepa function.

Secondly, it is polymorphic, but not only by type, but also by varieties of these types. This is indicated by a part forall k1 k2 (a :: k1) (b :: k2)- this means that athey bcan be not only ordinary types like Intor [String], but, for example, well-trained constructors (see DataKinds and other attempts to make a Haskell authenticated). But we don’t need all this.

Thirdly, it accepts two runtime representations of potentially different types, TypeRep aand TypeRep b.

Fourth, it returns a type value Maybe (a :~~: b). The most interesting thing happens here.

If the types do not match, then the function returns normal Nothing, and everything is fine. If the types do match, then the function returns Just valwhere it valhas the type a :~~: b. Let's see what type it 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 talk. Suppose we get a valtype value a :~~: b. How could it be built? The only way is with the help of the constructor HRefl, and this constructor requires :~~:the same on both sides of the icon . So it acoincides with b. Moreover, if we are pattern-tied for val, then the tympher will also know about it. Therefore, yes, the function eqTypeRepreturns the proof that two potentially different types coincide if they are actually equal.

However, in the paragraph above, I lied. No one is stopping us from writing in Haskell something like

wrong :: Int :~~: String
wrong = wrong   -- уау бесконечная рекурсия

or

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

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

That is why in the piece of documentation cited just above, the terminating value is mentioned . Both versions of the implementation wrongabove do not produce this terminating value, which gives us a little reason and confidence: if our program on the Haskell terminated (and did not come across undefined), then its result corresponds to the types written. 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 Haskell weakness in the code above is the type of 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 actually equal, but would also prove their inequality if they are actually unequal. The inconsistency of the Haskell logic, however, makes such functions a little pointless: it is all important when you use the language as a prover of theorems, and not as a programming language, and do not use Haskell as a prover.

Oh well, enough of the log and type theory, let's get back to our metrics. Now just draw an owl The discussion above hints that it is enough to store in our existential type also this is the most runtime representation of the type, and everything will be fine.

This leads us to the following 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 takes the following:

1. two type values Dyn;
2. a function that produces something for two values ​​of any type ,
   based only on the Dynconstants mentioned during creation (it is responsible for this forall),
   and which is called if both Dynstore values ​​of the same type;
3. and the fallback function, which is called instead of the previous one, if the types are still 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- This is an existential wrapper over TypeRep afor anyone a.

Now we can implement, for example, equality checking and comparison:

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

Here we took advantage of the fact that SomeTypeRepwe can compare with each other, so the fallback function for ordering also compare.

Done.

Только вот теперь грех не обобщить: заметим, что внутри Dyn, toDyn, withDyns мы никак не используем конкретно Ord, и это мог бы быть любой другой набор констрейнтов, поэтому мы можем включить расширение ConstraintKinds и обобщить, параметризовав Dyn конкретным набором ограничений, которые нам нужны в нашей конкретной задаче:

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

Тогда Dyn Ord будет нашим искомым типом, а, скажем, Dyn Monoid позволит хранить произвольные моноиды и что-то моноидальное с ними делать.

Напишем нужные нам инстансы для нашего нового Dyn:

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

… только вот это не работает. Тайпчекер не знает, что Dyn Ord также реализует Eq,
поэтому придётся копировать всю иерархию:

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

Ну, теперь точно всё.

... perhaps, in a modern Haskell, you can make it so that the timer itself displays instances of the form

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

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

And also, if you carefully squint, you can see that ours Dynlooks suspiciously like a dependent pair of species (ty : Type ** val : ty)from cryptic languages. But only in languages ​​known to me it is impossible to match the type, because parametricity (which in this case, IMHO, is interpreted too broadly), but here it seems possible.

But the most important thing - now you can safely have something like Map (Dyn Ord) SomeValueand use any values ​​as keys, as long as they themselves support the comparison. For example, identifiers with metric descriptions can be used as keys, but this is a topic for the next article.