search

nikita-volkov / refined

Refinement types with static checking
http://hackage.haskell.org/package/refined
MIT License
182 stars 31 forks source link

Question: Values associated with refinement types #55

Closed rkaippully closed 4 years ago

rkaippully commented 4 years ago

I wonder if it makes sense to generalize the idea behind refined. Instead of a predicate associated with a type, what if we had an arbitrary property and an associated value like this?

class Property p x where
    type Associated p x
    validate :: Monad m -> p -> x -> RefineT m (Associated p x)

instance Property HasHTTPBody HTTPRequest where
    type Associated HasHTTPBody HTTPRequest = HTTPBody

    validate :: Monad m -> HasHTTPBody -> HTTPRequest -> RefineT m HTTPBody
    validate = ...

getBody :: Refined HasHTTPBody HTTPRequest -> HTTPBody
getBody = ...

The idea is that one could process the HTTP request and retrieve the body in the validate function once and store it in some associated data structure. Not all requests have a body, so the refinement could fail in the validate function. If it is successful, we get a Refined HasHTTPBody HTTPRequest which contains a cached HTTPBody with it. This helps to avoid the expensive retrieval/parsing of the body multiple times.

I understand this is probably not in the scope of refined. But I was wondering if something like this already exists.

nikita-volkov commented 4 years ago

As per the Wikipedia definition:

In type theory, a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type.

In other words, refinement types are not about transforming data, but about providing proofs that data satisfies certain conditions.

What you're describing seems to be about partial data transformation and providing a default instance of that transformation with a typeclass. This idea has been expressed and experimented with multiple times. E.g., see the "convertible" package. Generally though the whole idea of providing default transformations has been criticized in the community and hasn't proved to be useful in practice.

This problem space has also been approached in the optic libraries (e.g., "lens", "optics"). See the a Traversal or AffineTraversal abstractions.

chessai commented 4 years ago

Thanks for the answer @nikita-volkov. I am going to close this as I see it as outside the scope of this library. Nevertheless this is a good question.

chessai commented 4 years ago

I wonder if this is worth documenting? Seems like a natural question.

rkaippully commented 4 years ago

Thanks @nikita-volkov. Yes, this is not in the scope of refined and is certainly different from refinement types.

I don't think convertible/traversals cleanly cover what I am looking for. AffineTraversal is probably closest. But I don't see how to embed arbitrary effects (such as caching). Thank you for the pointers, I'll explore more.