有没有办法使用的类型级模式匹配，而不是定义一个类家族

问题描述：

HList.hs的方式

{-# LANGUAGE DataKinds  #-} 
{-# LANGUAGE GADTs   #-} 
{-# LANGUAGE PolyKinds  #-} 
{-# LANGUAGE TypeOperators #-} 
module HList where 

data HList :: (k -> *) -> [k] -> * where 
    Nil :: HList f '[] 
    (:&) :: !(f x) -> HList f xr -> HList f (x ': xr)

Snd.hs

{-# LANGUAGE DataKinds   #-} 
{-# LANGUAGE KindSignatures  #-} 
{-# LANGUAGE RankNTypes   #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TypeFamilies  #-} 
{-# LANGUAGE TypeOperators  #-} 
module Snd where 

import   HList 

hmap :: forall f g xs. (forall x. f x -> g x) -> HList f xs -> HList g xs 
hmap f = go 

    where 
    go :: HList f xs' -> HList g xs' 
    go Nil  = Nil 
    go (x :& xs) = f x :& go xs 

type family Snd x where 
    Snd '(a, b) = b 

type family MapSnd xs where 
    MapSnd '[] = '[] 
    MapSnd (y ': ys) = Snd y ': MapSnd ys 

hmap2 :: forall f g (xs :: [(*,*)]). (forall x. f x -> g (Snd x)) -> HList f xs -> HList g (MapSnd xs) 
hmap2 f = go 
    where 
    go :: HList f xs' -> HList g (MapSnd xs') 
    go Nil  = Nil 
    go (x :& xs) = f x :& go xs

NoSnd.hs

{-# LANGUAGE DataKinds   #-} 
{-# LANGUAGE KindSignatures  #-} 
{-# LANGUAGE RankNTypes   #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TypeFamilies  #-} 
{-# LANGUAGE TypeOperators  #-} 
module NoSnd where 

import   HList 

hmap :: forall f g xs. (forall x. f x -> g x) -> HList f xs -> HList g xs 
hmap f = go 
    where 
    go :: HList f xs' -> HList g xs' 
    go Nil  = Nil 
    go (x :& xs) = f x :& go xs 

type family MapSnd xs where 
    MapSnd '[] = '[] 
    MapSnd ('(_, y) ': ys) = y ': MapSnd ys 

hmap2 :: forall f g (xs :: [(*,*)]). (forall x a b. (x ~ '(a, b)) => f x -> g b) -> HList f xs -> HList g (MapSnd xs) 
hmap2 f = go 
    where 
    go :: HList f xs' -> HList g (MapSnd xs') 
    go Nil  = Nil 
    go (x :& xs) = f x :& go xs

Compil荷兰国际集团Snd.hs的作品，但在编译NoSnd.hs给

NoSnd.hs:27:20: error: 
    • Could not deduce: x ~ '(a0, x0) arising from a use of ‘f’ 
     from the context: xs' ~ (x : xr) 
     bound by a pattern with constructor: 
        :& :: forall k (a :: k -> *) (x :: k) (xr :: [k]). 
         a x -> HList a xr -> HList a (x : xr), 
       in an equation for ‘go’ 
     at NoSnd.hs:27:9-15 
     ‘x’ is a rigid type variable bound by 
     a pattern with constructor: 
      :& :: forall k (a :: k -> *) (x :: k) (xr :: [k]). 
       a x -> HList a xr -> HList a (x : xr), 
     in an equation for ‘go’ 
     at NoSnd.hs:27:9 
    • In the first argument of ‘(:&)’, namely ‘f x’ 
     In the expression: f x :& go xs 
     In an equation for ‘go’: go (x :& xs) = f x :& go xs 
    • Relevant bindings include x :: f x (bound at NoSnd.hs:27:9)

Snd.hs和NoSnd.hs之间的区别在于，在后者，而不是定义一个类家族Snd，我尝试直接解构类型。这发生在两个地方：MapSnd的定义和（参数为）hmap2的类型。

这两个问题是：有人可以解释类型错误;有没有办法写hmap2而不定义Snd类型的家庭？

谢谢。

您可以将MapSnd的第一个版本比第二个版本看作“lazier”。我相信你绝对需要这种懒惰，如果你想在'f'中变成多态就像那样。 – dfeuer

答

声明

exists a. x ~ '(a, b)

比声明

b ~ Snd x

例如稍强，给予

type family Any :: (*, *) where {}

它是有效的结论

Snd Any ~ Snd Any

但它是无效的结论

exists a. Any ~ '(a, Snd Any)

因为Any不与任何其他统一无论如何。

你对事物的类型的一种(*,*)索引的HList，但你不知道，每一个元素实际上有一种形式'(a,b)的，所以你不能那证明传递给函数你”重新给予。现在，如果您有一个较少多态的列表，其中元素类型以已知方式进行索引，那么您可以对元素进行模式匹配以获得所需内容。但是，这不是你所拥有的，而且也不那么一般和有用。用你现在的（工作）公式，传递的函数负责处理任何需要了解索引结构的信息。但那很好，知道f的结构比你更好。把你的奖金，并去！

有没有办法使用的类型级模式匹配，而不是定义一个类家族

相关推荐