在Haskell中，如何对多类型类型进行重新排序
在Haskell中，可以使用类型级别的编程技术来对多类型类型进行重新排序。具体而言，可以使用GHC的Data.Typeable和Data.Proxy模块来实现。
首先，我们需要定义一个类型级别的列表，用于表示多类型类型的顺序。可以使用GHC的TypeFamilies扩展来定义这个列表。例如，我们可以定义一个类型级别的列表List，其中包含了多个类型作为其元素：
{-# LANGUAGE TypeFamilies #-}
type family List (xs :: [*]) :: *
type instance List '[] = ()
type instance List (x ': xs) = (x, List xs)在上述代码中，List是一个类型族，它接受一个类型级别的列表作为参数，并返回一个类型。List '[]表示空列表，而List (x ': xs)表示非空列表，其中x是列表的头部元素类型，xs是列表的尾部元素类型列表。
接下来，我们可以定义一个类型级别的函数Reorder，用于对多类型类型进行重新排序。可以使用GHC的TypeApplications扩展来指定类型参数。例如，我们可以定义一个Reorder函数，接受一个类型级别的列表和一个目标类型作为参数，并返回重新排序后的类型级别的列表：
{-# LANGUAGE TypeApplications #-}
type family Reorder (xs :: [*]) (t :: *) :: [*]
type instance Reorder '[] t = '[]
type instance Reorder (x ': xs) t = Reorder' (FindIndex x xs) (x ': xs) t
type family Reorder' (n :: Maybe Nat) (xs :: [*]) (t :: *) :: [*]
type instance Reorder' Nothing xs t = xs
type instance Reorder' (Just n) xs t = Reorder'' n xs t
type family Reorder'' (n :: Nat) (xs :: [*]) (t :: *) :: [*]
type instance Reorder'' 0 (x ': xs) t = t ': xs
type instance Reorder'' n (x ': xs) t = x ': Reorder'' (n - 1) xs t
type family FindIndex (x :: *) (xs :: [*]) :: Maybe Nat
type instance FindIndex x '[] = Nothing
type instance FindIndex x (x ': xs) = Just 0
type instance FindIndex x (y ': xs) = AddMaybeOne (FindIndex x xs)
type family AddMaybeOne (n :: Maybe Nat) :: Maybe Nat
type instance AddMaybeOne Nothing = Nothing
type instance AddMaybeOne (Just n) = Just (n + 1)在上述代码中，Reorder是一个类型族，它接受一个类型级别的列表和一个目标类型作为参数，并返回一个重新排序后的类型级别的列表。Reorder通过调用Reorder'函数来实现。Reorder'函数根据目标类型在列表中的索引位置，调用Reorder''函数进行实际的重新排序操作。FindIndex函数用于查找目标类型在列表中的索引位置。AddMaybeOne函数用于将Maybe Nat类型的索引位置加一。
使用上述定义的Reorder函数，我们可以对多类型类型进行重新排序。例如，假设我们有一个类型级别的列表'[Int, Bool, Char]，我们可以调用Reorder函数来将Bool类型移动到列表的开头：
type ReorderedList = Reorder '[Int, Bool, Char] Bool在上述代码中，ReorderedList将被推导为'[Bool, Int, Char]。
总结起来，在Haskell中对多类型类型进行重新排序的步骤如下：
- 定义一个类型级别的列表，用于表示多类型类型的顺序。
- 定义一个类型级别的函数，接受一个类型级别的列表和一个目标类型作为参数，并返回重新排序后的类型级别的列表。
- 使用类型应用（TypeApplications）来调用上述定义的函数，对多类型类型进行重新排序。
请注意，以上代码仅为示例，实际使用时可能需要根据具体需求进行调整和扩展。另外，由于本回答要求不提及具体的云计算品牌商，因此无法给出腾讯云相关产品和产品介绍链接地址。
相关·内容
1回答
我正在尝试定义一种可以限制于Nat子集的类型。虽然我意识到一个简单的解决方案是使用常规的ADT，但我仍然很好奇这种类型是否可以用附带的FromJSON实例来定义。
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Test where
import Control.Mo
浏览 2提问于2017-05-24得票数 3
回答已采纳
1回答
用自己的证明充实约束求解器
haskell、ghc、type-families
我有以下类型的家庭：
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
data Nat = Z | S Nat
type family WrapMaybes (n :: Nat) (a :: *) :: *
type instance WrapMaybes Z a = a
type instance WrapMaybes (S n) a = Maybe (WrapMaybes n a)
这在很大程度上如预期的那样工作，例如WrapMaybes (S (S Z)) Int ~ Maybe (Maybe Int)。
现在，很明显(
浏览 1提问于2018-07-15得票数 1
回答已采纳
2回答
如何在Haskell中不打印任何内容
haskell
我正在尝试编写一个Haskell函数，它返回列表中的第一项。
h [] = Nothing
h (x:xs) = x
当我用一个空列表调用它时：
main = print (h [])
我得到了以下错误：
prog.hs:4:8:
No instance for (Show a0) arising from a use of `print'
The type variable `a0' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
浏览 3提问于2013-09-17得票数 5
回答已采纳
2回答
类型级别的nats与文字和内射继承者？(n字曲)
haskell、ghc、dependent-type
我正在将概括为一个n-ary组合，但我很难将界面做得很好。也就是说，我不知道如何在类型级别上使用数字文字，同时仍然能够对后继者进行模式匹配。
翻滚我自己的nats
使用卷我自己的nats，我可以让n-ary编写工作，但我只能将n作为迭代的后继，而不是文字：
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
浏览 4提问于2013-12-28得票数 14
回答已采纳
1回答
将任意数据类型具体化为(编译时已知的)值。
haskell、ghc、data-kinds、derivingvia
我希望能写出这样的东西：
reify (Proxy @True)) == True;
reify (Proxy @(Just 5)) == Just 5;
有可能通过一个全面的实施吗？我已经到了
class Reify (a :: k) where
reify :: Proxy a -> k
我不知道怎么写这个，除了手工写每个实例:一个实例表示True，一个实例表示False，等等。我不想全部手工编写，我也不想使用模板haskell为我编写。我能有一个例子来做吗？
或者可能还有别的方法？对我来说，用例是能够编写：
type DeriveHelper :: Settings ->
浏览 3提问于2022-02-23得票数 2
2回答
TypeNats与定制数据语句的问题
haskell
我一直在试验一种简单表达式语言的评估函数，主要是为了熟悉一些我以前从未使用过的Haskell扩展。最新的实验是使用DataKinds和TypeFamilies来统一一元和二进制运算符。经过一些麻烦之后，我使它工作，但只有当我代表的运算符，一个定制的定义自然物：
data NatT = ZeroT | SuccT NatT
如果我尝试使用TypeNats，编译器就无法匹配这些类型。下面是失败的版本。这是apply函数的第二行，编译器抱怨-- f到a的应用程序。错误是无法将Double -> FuncN (n - 1)与FuncN n匹配(这正是FuncN定义的第二行)。使用n+1和n代替n
浏览 11提问于2022-05-17得票数 1
1回答
HSpec无期望未编译
haskell、hspec
我正在学习Haskell和我写了这个函数：
safeHead :: [a] -> Maybe a
safeHead [] = Nothing
safeHead (x:xs) = Just x
我现在正在尝试用HSpec测试它：
import Test.Hspec
main :: IO ()
main = hspec spec
spec :: Spec
spec =
describe "safeHead" $
it "should return Nothing for empty list" $
safeHead [] `sho
浏览 3提问于2015-06-03得票数 3
回答已采纳
1回答
为长度索引列表实现拉链
haskell、data-kinds
我正在尝试实现一种用于长度索引列表的拉链，它将返回列表中的每一项，并与该元素被删除的列表配对。例如，对于普通列表：
zipper :: [a] -> [(a, [a])]
zipper = go [] where
go _ [] = []
go prev (x:xs) = (x, prev ++ xs) : go (prev ++ [x]) xs
所以
> zipper [1..5]
[(1,[2,3,4,5]), (2,[1,3,4,5]), (3,[1,2,4,5]), (4,[1,2,3,5]), (5,[1,2,3,4])]
我目前正在尝试为长
浏览 0提问于2013-07-06得票数 11
回答已采纳
1回答
使用类型系统检查输出和输入列表的长度
haskell、types、proof、dependent-type
假设一个长度为n的列表L交织在列表J中，长度为n+ 1。我们想知道，对于J的每一个元素，L的哪个邻居是更大的。下面的函数以L作为输入，并生成一个长度为n+ 1的列表K，使得K的_i_th元素是J的_i_th元素的理想邻居。
aux [] prev acc = prev:acc
aux (hd:tl) prev acc = aux tl hd ((max hd prev):acc)
expand row = reverse (aux row 0 [])
我可以非正式地向自己证明，这个函数(我最初用Ocaml写的)结果的长度大于输入的长度。但是我跳到了Haskell (我的一种新语言)，因为我对
浏览 4提问于2017-02-09得票数 12
回答已采纳
1回答
如何将归纳推理应用于`GHC.TypeLits.Nat`？
haskell、type-families、induction
考虑由Peano数字索引的通常向量长度的zip定义：
{-# language DataKinds #-}
{-# language KindSignatures #-}
{-# language GADTs #-}
{-# language TypeOperators #-}
{-# language StandaloneDeriving #-}
{-# language FlexibleInstances #-}
{-# language FlexibleContexts #-}
module Vector
wher
浏览 1提问于2018-08-19得票数 6
回答已采纳
2回答
为所有高阶类型声明一个类型
haskell、type-families、higher-kinded-types
我有种感觉，我在问不可能的事，但现在开始了。
我希望将类型构造函数与一个完全应用的版本--数字的类型级别的参数--与自然数相关联。下面是一个示例ghci会话及其所需的用途：
ghci> :kind! MKNumbered Maybe
MKNumbered Maybe :: *
= Maybe (Proxy Nat 1)
ghci> :kind! MKNumbered Either
MKNumbered Either :: *
= Either (Proxy Nat 1) (Proxy Nat 2)
为了减少上面的噪音，基本上我得到了如下的东西
Maybe >---->
浏览 2提问于2019-05-08得票数 1
回答已采纳
1回答
包括类型变量在内的类型级别计算
haskell、ghc、type-level-computation
最近，我与freer一起工作，我受到启发，尝试创建一种方法，允许使用类型级别的计算来组合任意的性函数，例如：
(+) :: Integer -> Integer -> Integer
x + y = ...
(>) :: Integer -> Integer -> Bool
x > y = ...
(sumGtThan5) :: Integer -> Integer -> Bool
sumGtThan5 x y = (+) ..> (>5)
我得到的是具体类型的函数，例如，下面的代码编译并允许组合函数。
-- source cod
浏览 4提问于2021-12-26得票数 1
回答已采纳
1回答
如何定义符合证明的类型级列表索引？
haskell、dependent-type、type-families
{-# language GADTs, KindSignatures, DataKinds, TypeApplications, TypeOperators,
TypeFamilies, PolyKinds, UndecidableInstances, RankNTypes, AllowAmbiguousTypes #-}
import GHC.TypeLits
我想用一个类型级Nat来索引一个类型级列表
type family Index (xs :: [a]) (k :: Nat) where
Index (x:xs) 0 = x
Index (x:xs) k =
浏览 7提问于2021-02-18得票数 4
1回答
向GHC证明一个类型不等式
haskell、dependent-type、gadt、type-families、singleton-type
出于教育目的，我一直在尝试通过使用各种语言扩展和单例类型在Haskell中重建“使用Idris进行类型驱动的开发”(即)一书中的一个示例。它的要点是一个从非空向量中删除元素的函数，只要证明该元素确实在向量中。以下代码是自包含的(GHC 8.4或更高版本)。问题出现在最后：
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDerivin
浏览 20提问于2018-08-19得票数 10
回答已采纳
1回答
关于类型水平自然数的排序
haskell、types
我一直试图使用DataKinds扩展在Haskell中实现类型级的自然状态。到目前为止，我的代码如下所示：
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
-- the kind of natural numbers
data Nat = Zero | Succ Nat
-- type synonyms for the naturals
type N0 =
浏览 1提问于2014-09-25得票数 4
回答已采纳
1回答
快速检查有关长度索引列表的属性
haskell、dependent-type、quickcheck
我正在尝试使用QuickCheck测试Haskell中有关长度索引列表(a.k.a向量)的属性。我的问题是，GHC抱怨Show函数的main约束上出现了一个不明确的变量。
我已经用标准的方式定义了向量
data Nat = Z | S Nat
data Vec :: Nat -> * -> * where
Nil :: Vec 'Z a
(:>) :: a -> Vec n a -> Vec ('S n) a
vlength :: Vec n a -> Int
vlength Nil = 0
vlength (_ :>
浏览 3提问于2016-09-28得票数 3
回答已采纳
2回答
检查一个类型级别的列表是否包含另一个类型级别的列表。
haskell
如果一个类型级别的列表包含另一个类型级别的列表，那么可以编写返回True的类型级函数吗？
以下是我的尝试：
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module TypePlayground where
import Data.Type.Bool
type family InList (x :: *) (xs :: [*]) where
InList x '[]
浏览 4提问于2016-07-05得票数 7
回答已采纳
1回答
类型级函子只是2类的函子吗？
haskell、category-theory
据我所知，范畴的典型解释是，该范畴的对象是Haskell类型，而态射是Haskell函数。
根据这一解释：
{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
data Nat = Z | S Nat
type family Map (f :: Nat -> Nat) (x :: [Nat]) :: [Nat] where
Map f '[] = '[]
Map f (x ': xs) = (f x) ': (Map f (xs))
我们可以将Z解释为Hask的单个对象子范畴，将S a解释为函子
浏览 3提问于2014-11-11得票数 3
2回答
为什么我们使用折叠将数据类型编码为函数？
haskell、functional-programming、algebraic-data-types、church-encoding、scott-encoding
或者确切地说，为什么我们要使用foldr编码列表和迭代来编码数字呢？
不好意思，长时间的介绍，但我真的不知道如何命名，我想要问的东西，所以我需要先做一些说明。这在很大程度上来自于，它不能完全满足我的好奇心，而且我还会用秩n类型和无限懒惰的东西来处理这些问题。
将数据类型编码为函数的一种方法是创建一个“模式匹配”函数，该函数接收每个情况下的一个参数，每个参数都是接收与该构造函数对应的值的函数，以及返回相同结果类型的所有参数。
对于非递归类型，这一切都是按预期计算的。
--encoding data Bool = true | False
type Bool r = r -> r ->
浏览 6提问于2012-11-27得票数 16
回答已采纳
2回答
异构列表长度中的歧义类型变量
haskell
在计算异构列表的长度时，我遇到了不明确类型变量的问题。问题似乎是长度函数在HList的元素中不是多态的。
我的密码
首先，我使用的所有语言扩展：
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
浏览 1提问于2016-05-07得票数 4
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
即时通信 IM
ICP备案
对象存储
实时音视频活动推荐
腾讯云开发者
