首页
学习
活动
专区
工具
TVP
发布
社区首页 >问答首页 >是否可以使用Haskell的类型系统(GADT)来进行某种多态变体?

是否可以使用Haskell的类型系统(GADT)来进行某种多态变体?
EN

Stack Overflow用户
提问于 2018-10-10 05:24:39
回答 1查看 93关注 0票数 4

以下是我试图实现的目标:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

module Action where

import Data.Type.Set

data Configuration
  = A
  | B
  | C

data Action (configuration :: Configuration) where
  Action1 :: Member cfg '[ 'A ]     => Action cfg
  Action2 :: Member cfg '[ 'B, 'C ] => Action cfg
  Action3 :: Member cfg '[ 'A, 'C ] => Action cfg

exhaustive :: Action 'A -> ()
exhaustive Action1 = ()
exhaustive Action3 = ()

我有一组动作和一组配置,但有些动作只有在某些配置中才有意义。我不希望在配置中显式地丢弃不相关的操作,所以我考虑使用GADT。不幸的是,类型检查器不能意识到我的exhaustive函数确实是详尽的。

我想知道是否可以使用任何现有的类型级别列表/集,甚至行类型(就像在http://hackage.haskell.org/package/row-types-0.2.3.0/docs/Data-Row-Variants.html中一样)来解决这个问题。

我还尝试了一种方法,将Action2 :: Action '[ 'B, 'C ]和将类型类约束推送到exhaustive中,但都没有成功。

谢谢你的建议!(或者甚至是为什么这是一个糟糕的想法,或者不容易实现的原因)

EN

回答 1

Stack Overflow用户

发布于 2018-10-10 06:34:19

一位朋友提出了一个解决方案:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Action where

type family MemberB (x :: k) (l :: [k]) where
  MemberB x '[]     = 'False
  MemberB x (x:xs)  = 'True
  MemberB x (x':xs) = MemberB x xs

type Member x xs = MemberB x xs ~ 'True

data Configuration
  = A
  | B
  | C

data Action (configuration :: Configuration) where
  Action1 :: Member cfg '[ 'A ]     => Action cfg
  Action2 :: Member cfg '[ 'B, 'C ] => Action cfg
  Action3 :: Member cfg '[ 'A, 'C ] => Action cfg

exhaustive :: Action 'A -> ()
exhaustive Action1 = ()
exhaustive Action3 = ()
exhaustive Action2 = ()

显然,问题是我使用的Member (来自Data.Type.Set)不是closed类型的家族。现在,错误消息不是很好,我们尝试执行以下操作:

type family MemberB (x :: k) (l :: [k]) where
  MemberB x '[]     = TypeError ('Text "not a member")
  MemberB x (x:xs)  = 'True
  MemberB x (x':xs) = MemberB x xs

但不幸的是,这会导致类型错误!是因为TypeError会很高兴地与'True统一吗?如果有人有一个解决方案可以让类型错误稍微好一点,我很乐意接受!

为此,我提出了一个单独的问题:

How to define a custom type error within a type family for a constraint that uses type equality?

票数 3
EN
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接:

https://stackoverflow.com/questions/52729542

复制
相关文章

相似问题

领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档