函数的类型是否可以限制为某些提升的数据构造函数？

html5 • • 问答

我正试图将我的头围绕在提升的数据构造函数上。我特别想知道它们在不涉及类型系列和 GADT 的上下文中是否有用。所以我试图考虑是否可以使用它们来限制某个函数可以采用的术语级别值。例如，是否可以定义一个仅接受所有True术语列表的函数。以下将不起作用，因为(->)它是来自Typeto的函数Type并且'[ 'True]具有 kind [Bool]：

allTrue :: '[ 'True] -> Int
allTrue = length

但是我想知道是否可以使用提升的数据构造函数'True来定义这样的函数。此外，这样的定义是否总是需要 GADT 和/或类型族？

回答

您通常可以避免使用更高等级的类型的 GADT，尽管它会非常不方便。

{-# language RankNTypes, FunctionalDependencies, FlexibleInstances, ScopedTypeVariables #-}
import qualified Control.Category as C
import Data.Functor.Identity

newtype Same a b = Same {unSame :: forall f. f a -> f b}

coerceWith :: Same a b -> a -> b
coerceWith (Same f) = runIdentity . f . Identity

newtype Flip p a b = Flip {unFlip :: p b a}

refl :: Same a a
refl = Same id

sym :: Same a b -> Same b a
sym (Same f) = unFlip . f . Flip $ refl

trans :: Same a b -> Same b c -> Same a c
trans (Same f) (Same g) = Same (g . f)

instance C.Category Same where
  id = refl
  (.) = flip trans

-- Constraint-based sameness

-- The fundeps improve inference
class Sam a b | a -> b, b -> a where
  mas :: f a -> f b
instance Sam a a where
  mas = id

same :: Sam a b => Same a b
same = Same mas

newtype Gum a b = Gum
  { unGum :: forall r. (Sam a b => r) -> r }

withSame :: Same a b -> (Sam a b => r) -> r
withSame (Same s) = unGum $ s (Gum id)

symSam :: forall a b r pa pb. Sam a b => pa a -> pb b -> (Sam b a => r) -> r
symSam _ _ p = withSame (sym same :: Same b a) p

transSam :: forall a b c r pa pb pc. (Sam a b, Sam b c) => pa a -> pb b -> pc c -> (Sam a c => r) -> r
transSam _ _ _ p = withSame (trans (same :: Same a b) (same :: Same b c)) p

回答

要回答您的具体问题：不，没有类型的值是仅包含True. 提升的构造函数'True只是另一种类型，但因为它不是那种类型Type，所以它没有任何值。

回答您更普遍的问题：是的，即使没有类型系列和 GADT，也可以使用提升的类型构造函数。幻影类型是类型参数根本不出现在其值中的类型。您可以使用它们让类型系统为您做一些簿记。例如，假设您想跟踪是否在 中对 HTML 进行了转义String，以避免注入攻击。你可以这样写：

data IsEscaped = Escaped | NotEscaped

newtype UserText (e :: IsEscaped) = UserText { getUserText :: String }

fromRawUserText :: String -> UserText 'NotEscaped
fromRawUserText = UserText

escape :: UserText 'NotEscaped -> UserText 'Escaped
escape (UserText s) = UserText (escapeHTML s)

然后，您可以从该模块输出的类型UserText和功能fromRawUserText，escape以及getUserText，但不是在UserText构造函数。现在你有一个类型来跟踪它是否已经被转义。这将是调用错误escape在String一个已经逃出来了，也通过一项UserText 'NotEscaped向被期待的功能UserText 'Escaped。

你可以用类似的东西完成同样的事情

data NotEscaped
data Escaped
data UserText a = ...

但是您丢失了UserText应该使用Escapedor实例化的类型信息NotEscaped。所以这本质上是类型级别的无类型编程。提升的数据构造函数允许您在类型级别进行类型化编程。

以上是函数的类型是否可以限制为某些提升的数据构造函数？的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>