Замена самодельных Naturals литералами уровня типа GHC - PullRequest
Новая
       67

Замена самодельных Naturals литералами уровня типа GHC

0 голосов
/ 03 июля 2018

Я написал некоторый код, который принимает гетерогенный список и индексирует его. 

{-# 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 существует исключительно для повышения до Доброго уровня, а 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 достаточно прост: 

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, так как index принимает Proxy, но я не знаю, как заставить его быть правильным типом.

1 Ответ

0 голосов
/ 03 июля 2018

Как насчет этого? 

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
...