依赖类型的ghc-7.6类实例 [英] ghc-7.6 class instances for dependent types

问题描述

  data HList :: [ *]  - > *其中
 HNil :: HList'[] 
 HCons :: a  - > HList t  - > HList（a'：t）
  

示例列表li编译得很好：

$ （HConsInteger：（HCons 129877645 HNil）））

显然我们希望HList在Show类中，但我只能想出使用相互递归约束的以下工作类实例化（超类）：

  instance Show（HList'[]）where 
 show HNil =[]
 
 instance（Show a，Show'（HList t））=>显示（HList（a'：t））其中
 show l =[++ show'l ++]
 
 class显示'a where 
 show' :: a  - >字符串
 
实例显示'（HList'[]）其中
显示'HNil =
 
实例（Show a，Show'（HList t））= >显示'（HList（a'：t））其中
显示'（HCons h l）=情况l 
 HNil  - >显示h 
 HCons _  -   - > show h ++，++（show'l）
  

正确显示。需要编译的标志是：

  { - ＃LANGUAGE DataKinds，TypeOperators，KindSignatures，
 FlexibleContexts，GADTs，FlexibleInstances＃ } 
  

我尝试了许多以下更直接定义的变体，但是如果没有我能够理解ghc错误消息：

pre code> instance Show（HList'[]）where
show HNil = []

instance（Show a，Show（HList t））=>显示（HList（a'：t））其中
show l =[++（show'l）++]其中
显示'（HCons hs）= $ s $ b HNil - >显示h
HCons _ - - > show h ++，++（show's s）

某些Haskell / ghc专家可能会理解为什么这样做不起作用，我很乐意听到原因。

谢谢

Hans Peter

---

非常感谢哈马尔，为您提供了两个很好的工作示例，改进了我的第一个示例。

但我仍不明白为什么我的第二个例子不起作用。你说... show只知道如何显示当前的元素类型，而不是剩余的元素。但是，这个评论是否也不适用于以下（工作）代码：

  instance Show（HList'[]）where show HNil =
 
 instance（Show a，Show（HList t））=>显示（HList（a'：t））其中
显示（HCons h t）= t 
 HNil  - >显示h 
 HCons _  -   - > show h ++，++（show t）
  

解决方案

<正如Nathan在评论中所说的， show'只知道如何显示当前的元素类型，而不是剩余的元素类型。

在第一个例子中，我们可以通过为 show'创建一个新类型类来解决这个问题，尽管您只能使用一个显示实例：

   - 专业化显示'到HLists避免需要显示'（HList ts）约束
  - 在这里，这将需要UndecidableInstances。 
 instance（Show'ts）=>显示（HList ts）其中
显示xs =[++ show'xs ++]
 
 class显示'ts where 
 show':: HList ts  - >字符串
 
实例显示''[]其中
显示'HNil =
 
实例（Show a，Show'ts）=>显示'（a'：ts）其中
显示'（HCons a s）=案例s 
 HNil  - >显示
 HCons {}  - > show a ++，++ show's 
  

另一种更加恶意的方式来获得所有必要的显示约束到 show'将直接使用 ConstraintKinds 建立所有必要约束的列表。

   - 除原始代码中的扩展外：
 { - ＃LANGUAGE TypeFamilies，ConstraintKinds，UndecidableInstances＃ - } 
 import GHC.Exts 
 
  -  ShowTypes [a，b，c，...] =（显示a，显示b，显示c，...）
类型显示类型（a :: [*]）::约束
类型实例ShowTypes'[] =（）
类型实例ShowTypes（a'：t） =（Show a，ShowTypes t）
 
 instance ShowTypes ts => Show（HList ts）where 
 show xs =[++ show'xs ++]
 where 
 show':: ShowTypes ts => HList ts  - >字符串
显示'HNil =
显示'（HCons h s）=案例s 
 HNil  - >显示h 
 HCons {}  - > show h ++，++ show's 
  




Heterogeneous lists are one of the examples given for the new dependent type facility of ghc 7.6:

data HList :: [*] -> * where
  HNil :: HList '[]
  HCons:: a -> HList t -> HList (a ': t)

The example list "li" compiles fine:

li  = HCons "Int: " (HCons 234 (HCons "Integer: " (HCons 129877645 HNil)))

Obviously we would like HList to be in the Show class, but I can only come up with the following working class instantiation that uses mutually recursive constraints (superclasses):

instance Show (HList '[]) where 
  show HNil = "[]"

instance (Show a, Show' (HList t)) => Show (HList (a ': t)) where
  show l  = "[" ++ show' l ++ "]"

class Show' a where
  show' :: a -> String

instance Show' (HList '[]) where
  show' HNil = ""

instance (Show a, Show' (HList t)) => Show' (HList (a ': t)) where
  show' (HCons h l) = case l of
    HNil      -> show h
    HCons _ _ -> show h ++ ", " ++ (show' l)

The code compiles fine and li is shown properly. Compile flags needed are:

{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, 
FlexibleContexts, GADTs, FlexibleInstances #-}

I tried many variants of the following far more direct definition, but it doesn't compile without me being able to understand the ghc error messages:

instance Show (HList '[]) where 
  show HNil = "[]"

instance (Show a, Show (HList t)) => Show (HList (a ': t)) where
  show l  = "[" ++ (show' l) ++ "]" where  
    show' (HCons h s) = case s of
      HNil      -> show h
      HCons _ _ -> show h ++ ", " ++ (show' s)

Some Haskell / ghc specialist might understand why this can't work and I would be happy to hear the reason.

Thank you

Hans Peter

---

Thank you, hammar, for your two nice working examples, improving on my first example.

But I still don't understand why my second example doesn't work. You say that "... show' only knows how to show the current element type and not the remaining ones." But wouldn't that comment not also apply in the following (working) code:

instance Show (HList '[]) where show HNil = "" 

instance (Show a, Show (HList t)) => Show (HList (a ': t)) where 
   show (HCons h t) = case t of
      HNil      -> show h 
      HCons _ _ -> show h ++ ", " ++ (show t) 

解决方案

As Nathan said in the comments, show' only knows how to show the current element type and not the remaining ones.

As in your first example, we can get around this by making a new type class for show', although you can get away with only one Show instance:

-- Specializing show' to HLists avoids needing a Show' (HList ts) constraint
-- here, which would require UndecidableInstances.
instance (Show' ts) => Show (HList ts) where
  show xs = "[" ++ show' xs ++ "]"

class Show' ts where
  show' :: HList ts -> String

instance Show' '[] where
  show' HNil = ""

instance (Show a, Show' ts) => Show' (a ': ts) where
  show' (HCons a s) = case s of
    HNil     -> show a
    HCons {} -> show a ++ ", " ++ show' s

Another more hackish way of getting all the necessary Show constraints into show' is to use ConstraintKinds to directly build a list of all the necessary constraints.

-- In addition to the extensions in the original code:
{-# LANGUAGE TypeFamilies, ConstraintKinds, UndecidableInstances #-}
import GHC.Exts

-- ShowTypes [a, b, c, ...] = (Show a, Show b, Show c, ...)
type family ShowTypes (a :: [*]) :: Constraint
type instance ShowTypes '[] = ()
type instance ShowTypes (a ': t) = (Show a, ShowTypes t) 

instance ShowTypes ts => Show (HList ts) where
  show xs = "[" ++ show' xs ++ "]"
    where
      show' :: ShowTypes ts => HList ts -> String
      show' HNil = ""
      show' (HCons h s) = case s of
        HNil     -> show h
        HCons {} -> show h ++ ", " ++ show' s

这篇关于依赖类型的ghc-7.6类实例的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！