在Idris教程中,用于过滤矢量的函数基于从属对.
filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter f [] = (_ ** [])
filter f (x :: xs) with (filter f xs )
| (_ ** xs') = if (f x) then (_ ** x :: xs') else (_ ** xs')
但是为什么有必要把这个用于依赖对而不是更直接的东西呢？
filter' : (a -> Bool) -> Vect n a -> Vect p a
在这两种情况下,p必须确定类型,但在我假设的替代方案中,列出p两次列表的冗余被消除.
我实施的天真尝试filter'失败了,所以我想知道它是否存在无法实施的根本原因？或者可以filter'实施,也许filter只是在伊德里斯展示依赖对的一个不好的例子？但如果是这种情况那么在什么情况下依赖对会有用呢？
谢谢!
我正在使用Network.Pcap(pcap)进行一些网络捕获,并计划使用Net.PacketParsing(网络中心)进行一些检查.为此,看起来我必须将我的数据包解析
Pcap.Callback :: PktHdr -> Ptr Word8 -> IO ()
要么
Pcap.CallbackBS :: PktHdr -> ByteString -> IO ().
并将数据包作为'Ptr Word8'或'ByteString'处理.在数据包解析方面,我有:
Net.Packet.toInPack :: UArray Int Word8 -> InPacket
获得InPacket解析所需的类型.那么,剩下的就是将'Ptr'或'ByteString'转换为'UArray' - 无论是纯粹还是IO.我想我可以拆开ByteString来[Word8],并从那里到UArray,但好像必须有一个更好的办法.
我也很关心我选择的库.我过去曾经使用过网络设备并发现它非常好,但它已经老了并且使用了UArray,它本身看起来有点陈旧.因此欢迎提出更好的起点建议.
是否可以通过类型族或其他方式为任意类型匹配类型参数？
我试图写一个类型函数
type family Match s t a
它采用两个结构，s和t（假设它们具有相同类型的两个不同参数化，例如Maybe Int和Maybe String）和一个将与之匹配的参数。如果找到匹配的参数，类型函数将提供替换项。否则，它将提供原始参数。
Match (Maybe a) (Maybe b) a ~ b
Match (Maybe a) (Maybe b) c ~ c
我尝试的实现：
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
import Data.Type.Equality
import Data.Type.Bool
type family Match (s::k) (t::k) (a :: * ) :: * where
Match (f a :: *) (g b :: *) c = If ((a == c)) b c
找到参数后，该系列显然按计划工作：
> :t …