haskell - 用 GHC 类型级文字替换自建 Naturals

Question

我编写了一些采用异构列表并为其编制索引的代码。

{-# Language GADTs, FunctionalDependencies, MultiParamTypeClasses, KindSignatures, DataKinds, TypeOperators, FlexibleInstances, UndecidableInstances #-}

import Data.Kind

data Nat = Z | S Nat

data Natural a where
  Zero :: Natural 'Z
  Succ :: Natural a -> Natural ('S a)

data HList a where
  EmptyList :: HList '[]
  Cons :: a -> HList b -> HList (a ': b)

class IndexType (n :: Nat) (a :: [Type]) (b :: Type) | n a -> b where
  index :: (Natural n) -> (HList a) -> b

instance IndexType 'Z (a ': b) a where
  index _ (Cons a _) = a

instance IndexType a b c => IndexType ('S a) (d ': b) c where
  index (Succ a) (Cons _ b) = index a b

为此，我实现了自己的 Nat和 Natural类型。 Nat存在只是为了提升到 Kind 级别和 Natural存在满足种类 Nat -> Type .

现在我更愿意使用 GHC.TypeLits ' Nat亲切而不是我自己的然而，当我尝试翻译我的代码时，我开始在理解方面遇到困难。

我想建立我的 IndexType类和声明行不会改变任何

class IndexType (n :: Nat) (a :: [Type]) (b :: Type) | n a -> b where

自 GHC.TypeLits也有自己的 Nat种类。然而 GHC.TypeLits没有 Natural 的替代品我所看到的，即我缺乏这样的东西 Nat -> Type .现在我可以建立一个等效的

data Natural a = Natural

但这本质上等同于 Proxy键入这样我就可以使用它了。

{-# Language GADTs, FunctionalDependencies, MultiParamTypeClasses, KindSignatures, DataKinds, TypeOperators, FlexibleInstances, UndecidableInstances #-}

import Data.Kind
import GHC.TypeLits
import Data.Proxy

data HList a where
  EmptyList :: HList '[]
  Cons :: a -> HList b -> HList (a ': b)

class IndexType (n :: Nat) (a :: [Type]) (b :: Type) | n a -> b where
  index :: (Proxy n) -> (HList a) -> b

现在是 IndexType 的第一个实例类(class)很简单:

instance IndexType 0 (a ': b) a where
  index _ (Cons a _) = a

然而，第二个开始让我困惑。第一行似乎是

instance IndexType a b c => IndexType (1 + a) (d ': b) c where

但是在第二行我不知道如何替换 Succ在原始代码中。 Proxy 的数据构造函数是 Proxy所以我想它必须使用那个构造函数，所以我必须写一些类似的东西:

  index Proxy (Cons _ b) = index a b

但现在我正在提取 a 的定义凭空。我想它必须是另一个 Proxy因为索引采用 Proxy ，但我不知道如何强制它成为正确的类型。

Answer 1

这个怎么样？

class IndexType (n :: Nat) (a :: [Type]) (c :: Type) | n a -> c where           
  index ::  (Proxy n) -> (HList a) -> c                                         
instance IndexType 0  (a ': b) a where                                          
  index _ (Cons a _) = a                                                        
instance {-# OVERLAPS #-} (IndexType (a-1) b c) => IndexType a (d ': b) c where 
  index _ (Cons _ b) = index (Proxy @(a-1)) b                                   

这将使用一些额外的扩展，包括 ScopedTypeVariables和 TypeApplications . PoC(在 GHC 8.2.2 上测试):

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Foo where
import Data.Kind
import GHC.TypeLits
import Data.Proxy

data HList a where
  EmptyList :: HList '[]
  Cons :: a -> HList b -> HList (a ': b)

class IndexType (n :: Nat) (a :: [Type]) (c :: Type) | n a -> c where
  index ::  (Proxy n) -> (HList a) -> c
instance IndexType 0  (a ': b) a where
  index _ (Cons a _) = a
instance {-# OVERLAPS #-} (IndexType (a-1) b c) => IndexType a (d ': b) c where
  index _ (Cons _ b) = index (Proxy @(a-1)) b

list :: HList '[Int, Bool]
list = Cons (5 :: Int) (Cons True EmptyList)
int :: Int
int = index (Proxy @0) list
bool :: Bool
bool = index (Proxy @1) list