是否有一种将约束应用于类型应用程序的通用方法？ [英] Is there a general way to apply constraints to a type application?

问题描述

评论由用户 2426021684 引导我调查是否有可能想出一个类型函数 F 使得 F c1 c2 fa 表明对于一些 f 和<$ c
$ b

1. a ：
   
   $ fa $ fa


2. c1 f


3. c2 a

事实证明，最简单的形式非常简单。但是，我发现编写一个poly-kinded版本非常困难。幸运的是，当我写这个问题时，我设法找到了一种方法。

b
$ b

  { - ＃LANGUAGE TypeFamilies＃ - } 
 { - ＃LANGUAGE Con​​straintKinds＃ - } 
 { - ＃LANGUAGE FlexibleContexts＃ - } 
 { - ＃LANGUAGE FlexibleInstances＃ - } 
 { - ＃LANGUAGE MultiParamTypeClasses＃ - } 
 { - ＃LANGUAGE UndecidableInstances，UndecidableSuperClasses＃ - } 
 { - ＃LANGUAGE PolyKinds＃ } 
 { - ＃LANGUAGE TypeOperators＃ - } 
 { - ＃LANGUAGE ScopedTypeVariables＃ - } 
 
模块ConstrainApplications其中
 
 import GHC.Exts（Constraint ）
 import Data.Type.Equality 
  

现在键入系列以解构任意类型的应用程序。

 类型系列GetFun a其中
 GetFun（f _）= f 
类型系列GetArg a其中
 GetArg（_ a）= a 
  

现在是一个非常通用的函数，一个回答这个问题。但是这允许一个涉及这两个组件的约束。

  type G（cfa ::（j  - > k） - > j  - >约束）（fa :: k）
 =（fa〜（GetFun fa :: j  - > k）（GetArg fa :: j）
，cfa（GetFun fa） （GetArg fa））
  

我不喜欢没有类匹配的约束函数，所以这里是一个一级版 G 。

  class G cfa fa => ; GC cfa fa 
 instance G cfa fa => GC cfa fa 
  

可以表达 F 使用 G 和一个辅助类：

  class（cf f，ca a）=> Q cf ca f a 
 instance（cf f，ca a）=> Q cf ca f a 
 
 type F cf ca fa = G（Q cf ca）fa 
 
 class F cf ca fa => FC cf ca fa 
 instance F cf ca fa => FC cf ca 
  

以下是 F


  t1 :: FC（（〜）Maybe）Eq a =>> a  - > a  - > Bool 
 t1 =（==）
 
  - 在这种情况下，我们将类型*解构为两次*：
  - 我们将`a`分隔为`ey`，然后将
  - `e`分隔成`任一x`。 
 t2 :: FC（FC（（〜）Either）Show）Show a =>> a  - >字符串
 t2 x =左p的情况x  - >显示p 
正确的p  - >显示p 
 
 t3 :: FC Applicative Eq a => a  - > a  - > GetFun a Bool 
 t3 x y =（==）< $> x * y 
  




A comment by user 2426021684 led me to investigate whether it was possible to come up with a type function F such that F c1 c2 fa demonstrates that for some f and a:

1. fa ~ f a
2. c1 f
3. c2 a

It turns out that the simplest form of this is quite easy. However, I found it rather difficult to work out how to write a poly-kinded version. Fortunately, I managed to find a way as I was writing this question.

解决方案

First, some boilerplate:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances, UndecidableSuperClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

module ConstrainApplications where

import GHC.Exts (Constraint)
import Data.Type.Equality

Now type families to deconstruct applications at arbitrary kinds.

type family GetFun a where
  GetFun (f _) = f
type family GetArg a where
  GetArg (_ a) = a

Now an extremely general type function, more general than necessary to answer the question. But this allows a constraint involving both components of the application.

type G (cfa :: (j -> k) -> j -> Constraint) (fa :: k)
  = ( fa ~ (GetFun fa :: j -> k) (GetArg fa :: j)
    , cfa (GetFun fa) (GetArg fa))

I don't like offering constraint functions without classes to match, so here's a first-class version of G.

class G cfa fa => GC cfa fa
instance G cfa fa => GC cfa fa

It's possible to express F using G and an auxiliary class:

class (cf f, ca a) => Q cf ca f a
instance (cf f, ca a) => Q cf ca f a

type F cf ca fa = G (Q cf ca) fa

class F cf ca fa => FC cf ca fa
instance F cf ca fa => FC cf ca fa

Here are some sample uses of F:

t1 :: FC ((~) Maybe) Eq a => a -> a -> Bool
t1 = (==)

-- In this case, we deconstruct the type *twice*:
-- we separate `a` into `e y`, and then separate
-- `e` into `Either x`.
t2 :: FC (FC ((~) Either) Show) Show a => a -> String
t2 x = case x of Left p -> show p
                 Right p -> show p

t3 :: FC Applicative Eq a => a -> a -> GetFun a Bool
t3 x y = (==) <$> x <*> y

这篇关于是否有一种将约束应用于类型应用程序的通用方法？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！