来自通用Integer表达式的TypeLit [英] TypeLit from generic Integer expression

问题描述

我知道构造Nat的唯一方法是将-XDataKinds与提升的整数(即type MyInt = 10 :: Nat)一起使用.

The only way I know to construct a Nat is to use -XDataKinds with promoted integers, i.e., type MyInt = 10 :: Nat.

相反，我想拥有一个功能

Instead, I'd like to have a function

foo :: Integer -> Integer

我可以用反射的Nat进行索引，然后 reify 结果.为了演示我的意思，请假设使用某些功能mkNat :: Integer -> Q Type.我想写

that I can index with a reflected Nat, and then reify the result. To demonstrate what I mean, assume some function mkNat :: Integer -> Q Type. I want to write

type Z = $(mkNat $ foo $ natVal (Proxy::Proxy 10))

(在我的示例中，foo足够快，可以在编译时进行计算，而不会产生过多开销.)具有此功能可以节省我在单独的GHCi会话中运行foo的多步骤过程，然后进行复制将结果的十进制表示形式转换为源文件，然后编译我真正想要的代码.

(In my example, foo is fast enough that it can be computed at compile time without prohibitive overhead.) Having this capability saves me the multi-step process of running foo in a separate GHCi session, then copying the decimal representation of the result into a source file, and then compiling the code I really wanted.

当然，唯一缺少的组件是mkNat.如果我编写自己的自定义数据类型，则很容易编写mkNat的等效项.但是我真的很想使用内置的TypeLits.是否有一些TemplateHaskell(或单例或其他魔术)可以让我将任意Integer表达式转换为Nat?

Of course the only missing component is mkNat. If I write my own custom data type, the equivalent of mkNat is easy to write. But I'd really like to use the built-in TypeLits. Is there some TemplateHaskell (or singletons, or some other magic) that would allow me to reify an arbitrary Integer expression to a Nat?

推荐答案

是的！

{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE TemplateHaskell #-}

module Main where

import Data.Proxy
import GHC.TypeLits
import Splices

type Z = $(mkNat $ natVal (Proxy :: Proxy 10))

然后:

module Splices where

import Language.Haskell.TH

mkNat :: Integer -> Q Type
mkNat = return . LitT . NumTyLit

这篇关于来自通用Integer表达式的TypeLit的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！