Comments (8)
You would still need the unsafeCoercing to construct an a :- b
from an a => Dict b
then.
Here's one way (I think) to do the unsafeCoercing (using the old definition of (:-)
)
I vote for naming subdict
implied
:
implied :: forall a b. (a => b) => a :- b
from constraints.
I am also in favor of adding implied
.
The change to (:-)
proposed in #41 (comment) is interesting, but it would require constraints
to cut off support for pre-8.6 versions of GHC. (Unless we were to employ some sort of CPP-based backwards-compatibility hack, which doesn't sound appealing.) Until then, adding implied
should be uncontroversial.
from constraints.
Wait! Does it require implication constraints
subdict :: forall a b. a `Implies` b => a :- b
subdict = Sub @a @b (Dict @a)
Is it completely equivalent or is one more powerful than the other? I makes sense that entailment is a reified version of implication constraints like these are reified versions of coercion, constraints, equality, ...
Coercion :: Coercible a b => Coercion a b
Dict :: a => Dict a
Refl :: a ~ b => a :~: a
HRefl :: a ~~ b => a :~~: b
If so then there is no way to write subdict
until we get implication constraints, feel free to close this.
from constraints.
There is no way to write this at present.
from constraints.
This is now possible with the WIP QuantifiedConstraints
branch of GHC:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
data Dict c where
Dict :: c => Dict c
newtype a :- b = Sub (a => Dict b)
subdict :: forall a b. (a => b) => a :- b
subdict = Sub (Dict @b)
from constraints.
This will probably have to wait until 8.6 or so before it can be added directly to the library. It seems like QuantifiedConstraints
will miss the 8.4 branch at this point.
from constraints.
Can't wait for QC. Going the other way ((a :- b) -> Dict (a => b)
) is not possible though
from constraints.
Building the other direction is a messy exercise in unsafeCoercing enough stuff to produce the right core. It is admissible.
But we could avoid that completely. In the presence of QuantifiedConstraints
the encoding I use for (:-)
is suboptimal. Switching from the existing Sub Dict
encoding to
data a :- b where
Sub :: (a => b) -> a :- b
or, equivalently,
newtype a :- b = Sub (Dict (a => b))
makes this easy though, giving a good reason to favor such an encoding over the current approach going forward.
from constraints.
Related Issues (20)
- Consider using AppendSymbol in Data.Constraint.Symbol HOT 3
- constraints-0.10.1 needs revision HOT 1
- An adjunction(?)
- constraints-0.11 and 0.11.1 need base < 4.16 revisions HOT 1
- Update for GHC 9.2 HOT 2
- Build failure with `mtl-2.3` HOT 1
- The `forall` function triggers `-Wforall-identifier` on GHC 9.4
- Use `withDict` instead of `unsafeCoerce` to implement `magic`
- Build failures with mtl-2.3 and `transformers < 0.6` HOT 2
- Add Data.Constraints.Char for GHCs where it is available. HOT 3
- constraints-0.13.1 cannot be build with GHC 9.4 HOT 1
- Soundness of `powMonotone2` HOT 1
- constraints-0.13.4 cannot be built with GHC 9.10 alpha 1 HOT 1
- dividesDef and timesDiv appear to have unsafe typos
- Expose ComposeC
- divideTimes' constraint is too tight
- Class instances HOT 4
- Update for QuantifiedConstraints
- Divides a b :- (Mod b a ~ 0) HOT 3
- instance Lift (Dict cls) HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from constraints.