# 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 `a`

that 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 `SomeOrd`

and 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 `val`

implements 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, `Ord`

it is necessary that and `val`

, and `val2`

have the same type, but this is absolutely not required to be performed! It turns out that ours is `SomeOrd`

useless. 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 `a`

is the value of the type `TypeRep a`

, and~~request~~generation is answered by a class `Typeable`

.

**By the way**

By the way, it `a`

does not have to be a type in the usual sense, that is, belong to a variety `*`

. It can be of any other kind `k`

, which theoretically allows you to do some cool things with storing runtime representatives of the learned types and the like, but I have not yet figured out what exactly.

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, `a`

coincides 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, `eqTypeRep`

a 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 `a`

they `b`

can be not only ordinary types like `Int`

or `[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 a`

and `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 val`

where it `val`

has 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 `val`

type 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 `a`

coincides with `b`

. Moreover, if we are pattern-tied for `val`

, then the tympher will also know about it. Therefore, yes, the function `eqTypeRep`

returns 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 `wrong`

above 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:

- two type values
`Dyn`

; - a function that produces something for two values of
*any type*,

based only on the`Dyn`

constants mentioned during creation (it is responsible for this`forall`

),

and which is called if both`Dyn`

store values of the same type; - 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 a`

for 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 `SomeTypeRep`

we 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 `Dyn`

looks 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) SomeValue`

and 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.