使用Data.Constraint.Forall具有等式约束 [英] Using Data.Constraint.Forall with equality constraints

问题描述

  { - ＃LANGUAGE ScopedTypeVariables＃ - } 
 
 class C a where 
 
 foo :: forall fa b。 （C（f a），C（f b））=> f a  - > fb 
 foo = _ 
  

现在，如果我想移动<$在$ foo a 和 b c>（假设我想用 foo 来实现一个类型类方法，它需要在 a 中是多态的）和 b ），可以使用 Data.Constraint.Forall ：

  { - ＃LANGUAGE ScopedTypeVariables＃ - } 
 { - ＃LANGUAGE Con​​straintKinds，TypeOperators＃ - } 
 import Data.Constraint 
 import Data.Constraint.Forall 
 
 foo':: forall f。 （ForallF C f）=>一个b。 f a  - > f b 
 foo'= helper 
其中
 helper :: forall a b。 f a  - > f b 
 helper = case（instF :: ForallF C f： -  C（f a））
 Sub Dict  - > 
的情况（instF :: ForallF C f：-C（f b））Sub Dict  - > foo 
  

现在，我的问题是，假设我将函数更改为涉及类型相等的东西：

  { - ＃LANGUAGE TypeFamilies，ScopedTypeVariables＃ - } 
 
 type family F a :: *  - > * 
 
 bar :: forall f g a b。 （F（f a）〜g a，F（f b）〜g b）=> f a  - > fb 
 bar = _ 
  

有没有办法让上述技术适应这个？ / p>

以下是我试过的：

  { - ＃LANGUAGE TypeFamilies，ScopedTypeVariables ＃ - } 
 { - ＃LANGUAGE Con​​straintKinds，TypeOperators＃ - } 
 import Data.Constraint 
 import Data.Constraint.Forall 
 
 type F'Eq fgx = F （fx）〜gx 
 
 bar':: forall f g。 （Forall（F'Eq f g））=>一个b。 f a  - > f b 
 bar'=助手
其中
 helper :: forall a b。 f a  - > f b 
 helper = case（inst :: Forall（F'Eq f g）： -  F'Eq f g a）of 
 Sub Dict  - > case（inst :: Forall（F'Eq f g）： -  F'Eq f g b）of 
 Sub Dict  - > bar 
  

但是（不出所料）这个失败是因为不饱和类型的同义词：

类型同义词'F'Eq'应该有3个参数，但已被赋予2

在表达式类型签名中： Forall（F'Eq fg）： - F'Eq fga

在表达式中：（inst :: Forall（F'Eq fg）： - F'Eq fga）

解决方案

您可以使用一个类：

  { - ＃LANGUAGE MultiParamTypeClasses，FlexibleInstances，FlexibleContexts＃ - } 
 
 class（F（fx）〜gx）=> F'Eq f g x 
 instance（F（f x）〜g x）=> F'Eq f g x 
 
 bar':: forall f g。 （Forall（F'Eq f g））=>一个b。 f a  - > f b 
 bar'=助手
其中
 helper :: forall a b。 f a  - > f b 
 helper = case（inst :: Forall（F'Eq f g）： -  F'Eq f g a）of 
 Sub Dict  - > case（inst :: Forall（F'Eq f g）： -  F'Eq f g b）of 
 Sub Dict  - > bar 
  

Let's say I have a function like this:

{-# LANGUAGE ScopedTypeVariables #-}

class C a where

foo :: forall f a b. (C (f a), C (f b)) => f a -> f b
foo = _

Now, if I would like to move the scope of a and b to the right of the typeclass constraint in the type of foo (let's say, because I want to use foo to implement a typeclass method that needs to be polymorphic in a and b), it can done with a bit of legwork using Data.Constraint.Forall:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds, TypeOperators #-}
import Data.Constraint
import Data.Constraint.Forall

foo' :: forall f. (ForallF C f) => forall a b. f a -> f b
foo' = helper
  where
    helper :: forall a b. f a -> f b
    helper = case (instF :: ForallF C f :- C (f a)) of
        Sub Dict -> case (instF :: ForallF C f :- C (f b)) of
            Sub Dict -> foo

Now, my question is, suppose I change my function to something involving type equalities:

{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}

type family F a :: * -> *

bar :: forall f g a b. (F (f a) ~ g a, F (f b) ~ g b) => f a -> f b
bar = _

Is there a way to adapt the above technique to this?

Here's what I tried:

{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds, TypeOperators #-}
import Data.Constraint
import Data.Constraint.Forall

type F'Eq f g x = F (f x) ~ g x

bar' :: forall f g. (Forall (F'Eq f g)) => forall a b. f a -> f b
bar' = helper
  where
    helper :: forall a b. f a -> f b
    helper = case (inst :: Forall (F'Eq f g) :- F'Eq f g a) of
        Sub Dict -> case (inst :: Forall (F'Eq f g) :- F'Eq f g b) of
            Sub Dict -> bar

But (unsurprisingly) this fails because of the unsaturated type synonym:

Type synonym ‘F'Eq’ should have 3 arguments, but has been given 2

In an expression type signature: Forall (F'Eq f g) :- F'Eq f g a

In the expression: (inst :: Forall (F'Eq f g) :- F'Eq f g a)

解决方案

You can use a class:

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}

class (F (f x) ~ g x) => F'Eq f g x
instance (F (f x) ~ g x) => F'Eq f g x

bar' :: forall f g. (Forall (F'Eq f g)) => forall a b. f a -> f b
bar' = helper
  where
    helper :: forall a b. f a -> f b
    helper = case (inst :: Forall (F'Eq f g) :- F'Eq f g a) of
        Sub Dict -> case (inst :: Forall (F'Eq f g) :- F'Eq f g b) of
            Sub Dict -> bar

这篇关于使用Data.Constraint.Forall具有等式约束的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！