Pull type-level value out of dependent type/using type-level bindings at value-level

user_834176 0
Viewed 224

When I have a dependent type in Haskell, how do I use the value stored in the type in a function? Example Haskell program that I would want to write (which does not compile, because the min and max typelevel bindings do not extend to value level):

{-# 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 can do this in 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

Which compiles and works as expected:

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

How do I translate this Idris program to Haskell without reducing the amount of information in the type?

data-kinds dependent-type gadt haskell
2 Answers

One possibility (however I am not convinced it is worth the trouble) is to index your CharRange with Natural numbers rather than the Char they encode.

This way you get use GHC.TypeNats to gain the ability to obtain a copy of these type levels bounds.

The worked out solution goes something like this:

{-# 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
user_7276670

If you do not want to do any fancy arithmetic on the bounds, but use them as configurable constants, enforcing an invariant throughout a computation, you can also use the reflection package.

The upside is that your constants do not have to be known at compile time. Have a look at the documentation for the reflection package to learn more. For example, there is an instance KnownNat n => Reifies (n :: Nat) Integer so there is some interoperability (in one direction, at least), e.g. using reifyNat instead of reify to configure your terms.

{-# 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 '_')
user_31029350
Related