从依赖类型中拉出类型级别值/在值级别使用类型级别绑定

Question

当我在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

我可以在伊德里斯做到这一点：

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？

Answer 1

[一种可能性（但是我不认为这是值得的麻烦）是用CharRange个数字而不是它们编码的Nat为您的Char编制索引。

通过这种方式，您可以使用GHC.TypeNats获得获得这些类型级别范围的副本的功能。

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

GHC.TypeNats