有沒有辦法使用的類型級模式匹配，而不是定義一個類家族

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類型的家庭？

謝謝。

來源

2017-10-05 Alex R

您可以將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的結構比你更好。把你的獎金，並去！

來源

2017-10-05 17:04:25 dfeuer

有沒有辦法使用的類型級模式匹配，而不是定義一個類家族

回答

相關問題