代码之家 › 专栏 › 技术社区 › Siddharth Bhat

秩2约束规划/约束蕴涵

types haskell

Siddharth Bhat · 技术社区 · 7 年前

import Data.Constraint

reify :: (c' :- c) -> (c => a) -> (c' => a)
reify cons f = case cons of Sub d -> case d of Dict -> f

使用 reify c c' 证明 c' .

现在,我想要一个 Rank2 这方面的变体:

-- reify2 Rank2's reify
reify2 :: (forall r1. c' r1 :- c r1) -> 
          (forall r2. c r2 => a) -> 
          (forall r3. c' r3 => a)
reify2 cons f = ???

1 回复 | 直到 7 年前

Li-yao Xia 7 年前

可以使用以下方法消除歧义: ScopedTypeVariables+TypeApplications reify2 ,将类型参数放在第一位以将其放入范围。

{-# LANGUAGE AllowAmbiguousTypes, RankNTypes, ConstraintKinds, GADTs, ScopedTypeVariables, TypeApplications, TypeOperators #-}

data Dict c where
  Dict :: c => Dict c

data c :- d where
  Sub :: (c => Dict d) -> c :- d

reify2 :: forall r3 c c' a. c' r3 =>
          (forall r1. c' r1 :- c r1) ->
          (forall r2. c r2 => a) ->
          a
reify2 cons f =
  case cons @r3 of
    Sub Dict -> f @r3

推荐文章

Gadzhiev Islam · 在typescript中如何将接口键声明为特定类型?

1 年前

Zachiah · 为什么在打字稿中设置动态键是不健全的

1 年前

Kris Craig · 为什么Comparer不支持C#中lambda操作的64位(长)委托返回类型?

1 年前

Thiago Pereira Maia · 验证对象键与值的字符串内容之间的相关性

1 年前

Thiago Souza · Angular:对象键可以通过组件脚本上的变量访问,但不能在HTML上访问

2 年前

CMTV · TypeScript类型提示类似于`document.createElement`

2 年前

Aaditya · 在c中声明具有指定类型的变量++

2 年前

blackthorne18 · 如何将R中的数据帧转换为“字符”数据类型?

2 年前

etblh · Typescript:如何通过函数参数的值获取提取的联合类型的属性

2 年前