Извлечение значения уровня типа из зависимого типа / использование привязок уровня типа на уровне значения

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

Iможно сделать это в 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, не уменьшая объем информации в типе?

Answer 1

Если вы не хотите делать какие-либо причудливые арифметические действия на границах, но используете их в качестве настраиваемых констант, применяя инвариант во время вычислений, вы также можете использовать пакет отражения.

Преимущество состоит в том, что вашконстанты не должны быть известны во время компиляции. Посмотрите документацию для пакета отражения , чтобы узнать больше. Например, есть экземпляр 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 '_')

Answer 2

Одна возможность (однако я не уверен, что это стоит того) состоит в том, чтобы индексировать ваши CharRange с помощью Nat уральных чисел, а не Char, которые они кодируют.

Таким образом, вы получаете использование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