从依赖类型中提取类型级值/在值级使用类型级绑定答案

【问题标题】：Pull type-level value out of dependent type/using type-level bindings at value-level从依赖类型中提取类型级值/在值级使用类型级绑定
【发布时间】：2019-10-03 21:18:05
【问题描述】：

当我在 Haskell 中有依赖类型时，如何在函数中使用类型中存储的值？我想编写的示例 Haskell 程序（无法编译，因为 min 和 max 类型级别绑定不会扩展到值级别）：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
module CharRange (CharRange, ofChar, asChar) where

data CharRange :: Char -> Char -> * where
  C :: Char -> CharRange min max

ofChar :: Char -> CharRange min max
ofChar c =
  if min <= c && c <= max
  then C c
  else C min

asChar :: CharRange min max -> Char
asChar (C c) =
  if min <= c && c <= max
  then c
  else min

我可以在 Idris 中做到这一点：

module CharRange

%default total
%access export

data CharRange : Char -> Char -> Type where
  C : Char -> CharRange min max

ofChar : Char -> CharRange min max
ofChar c =
  if min <= c && c <= max
  then C c
  else C min

asChar : CharRange min max -> Char
asChar (C c) =
  if min <= c && c <= max
  then c
  else min

按预期编译和工作：

λΠ> the (CharRange 'a' 'z') $ ofChar 'M'
C 'a' : CharRange 'a' 'z'
λΠ> the (CharRange 'a' 'z') $ ofChar 'm'
C 'm' : CharRange 'a' 'z'

如何在不减少类型信息量的情况下将此 Idris 程序翻译成 Haskell？

【问题讨论】：

Haskell 没有依赖类型。
扩展@chepner 的评论：您绝对可以使用singletons 之类的库以及各种语言特性来模拟依赖类型。然而，Haskell 本身（还）不支持依赖类型，所以即使你可以非常接近使用它们，你也不能以你尝试使用它们的相同方式实际使用依赖类型。
Char 类型不包含任何类型（尽管它确实包含许多值）。也就是说，目前写data CharRange :: Char -> Char -> Type 是没有用的（顺便说一句，* 已弃用，请使用Data.Kind 中的Type），因为对于某些x, y :: Char，您永远无法实际构造CharRange x y 类型。 DataKinds 基本上只适用于 ADT，加上（难以忍受的不稳定，IMO）内置插件 Nat 和 Symbol。
不，两边都是一样的Char。值有类型。类型有类型。我们有时会说“善良”这个词，这是一个历史偶然，因为过去有区别，现在没有了。 Char 是一个充满值但没有类型的类型的示例。 Type 是一个没有值但充满类型的类型的示例。大多数类型在两边都是相同的。
在 Haskell 中，当我们编写 ofChar : forall min max . .....etc etc 时，类型级参数 min 和 max 在类型检查期间使用，然后在运行时擦除（不像伊德里斯）。这意味着ofChar 在运行时不会收到有关min 和max 是什么的信息。为了避免这种情况，我们通常求助于singletons，并编写类似ofChar :: forall min max . SChar min -> SChar max -> ....etc etc 的内容，其中SChar c 是一个“单例”类型，它在运行时保留将丢失的信息。您会在 singletons 库中找到许多示例。

标签： haskell dependent-type gadt data-kinds

【解决方案1】：

一种可能性（但我不相信这值得麻烦）是用Natural 数字而不是它们编码的Char 来索引您的CharRange。

这样您就可以使用GHC.TypeNats 获得获得这些类型级别边界副本的能力。

制定的解决方案是这样的：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Ranged (CharRange, ofChar, asChar) where

import GHC.TypeNats
import Data.Char
import Data.Proxy

data CharRange :: Nat -> Nat -> * where
  C :: Char -> CharRange min max

ofChar :: forall min max. (KnownNat min, KnownNat max)
       => Char -> CharRange min max
ofChar c =
  let min = fromIntegral $ natVal (Proxy :: Proxy min) in
  let max = fromIntegral $ natVal (Proxy :: Proxy max) in
  if min <= fromEnum c && fromEnum c <= max
  then C c
  else C (toEnum min)

asChar :: forall min max. (KnownNat min, KnownNat max)
       => CharRange min max -> Char
asChar (C c) =
  let min = fromIntegral $ natVal (Proxy :: Proxy min) in
  let max = fromIntegral $ natVal (Proxy :: Proxy max) in
  if min <= fromEnum c && fromEnum c <= max
  then c
  else toEnum min

【讨论】：

欣赏这个选项和“不相信这是值得的麻烦”。

【解决方案2】：

如果您不想对边界进行任何花哨的算术运算，而是将它们用作可配置的常量，在整个计算过程中强制执行不变量，您也可以使用反射包。

好处是你的常量不必在编译时就知道。查看reflection package 的文档以了解更多信息。例如，有一个实例KnownNat n => Reifies (n :: Nat) Integer，因此存在一些互操作性（至少在一个方向上），例如使用reifyNat 而不是reify 来配置您的条款。

{-# LANGUAGE ScopedTypeVariables, TypeApplications, FlexibleContexts -#}
{-# LANGUAGE AllowAmbiguousTypes #-}
import Data.Reflection
import Data.Char
import Data.Proxy

newtype CharRange min max = C Char

--| this is the only thing that needs AllowAmbiguousTypes, but we don't need to write
-- Proxy everywhere. Choose your poison.
reflect' :: forall s a. Reifies s a => a
reflect' = reflect @s Proxy

ofChar :: forall min max. (Reifies min Char, Reifies max Char)
       => Char -> CharRange min max
ofChar c =
  if reflect' @min <= c && c <= reflect' @max
  then C c
  else C $ reflect' @min

asChar :: forall min max. (Reifies min Char, Reifies max Char)
       => CharRange min max -> Char
asChar (C c) =
  if reflect' @min <= c && c <= reflect' @max
  then c
  else reflect' @min

-- At the toplevel, you need to configure your 'constants'.
-- using reify you get Proxy parameters, that allows you to capture
-- the type variable that is used to reflect the arguments back inside
-- your computation.
-- this might seem like a lot of code, but since it's toplevel needs only
-- be done once.
main = print $ show $ reify 'a' $
            \(_ :: Proxy min) -> reify 'z' $
              \(_ :: Proxy max) -> asChar (ofChar @min @max '_')

【讨论】：