代码之家 › 专栏 › 技术社区 › nicolas

Haskell中的可见类型应用程序:如何绑定类型

type-level-computation types haskell

2

nicolas · 技术社区 · 6 年前

这允许删除以下值: Proxy :: Proxy s 只是为了绑定类型 s 当我们是一个用户时,我们只是写 myPolyValue @ s

但如果我们是 建筑物 一个多态值,除了一个类型的参数外,有没有办法绑定我们被调用的类型 Proxy s

实例我用 VisibleTypeApplication 代理服务器

#!/usr/bin/env stack
-- stack --resolver nightly-2018-12-12 script --package base-unicode-symbols --package unicode-prelude --package constraints
{-# LANGUAGE AllowAmbiguousTypes,GeneralizedNewtypeDeriving  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies, KindSignatures #-}
{-# LANGUAGE FlexibleContexts , TypeApplications #-}
{-# LANGUAGE InstanceSigs , FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses , ScopedTypeVariables #-}
{-# LANGUAGE GADTs , MultiParamTypeClasses     #-}
{-# LANGUAGE RankNTypes , TypeOperators             #-}
{-# LANGUAGE UnicodeSyntax,DataKinds              #-}

module ImplicitConfigurationFirstPart where

import Data.Proxy

data KNat where
  Zero :: KNat
  Twice :: KNat -> KNat
  Succ :: KNat -> KNat
  Pred :: KNat -> KNat

class ReflectNum (s :: KNat) where reflectNum â· Num a â Proxy s -> a
instance                ReflectNum  'Zero      where reflectNum _ = 0
instance ReflectNum s â ReflectNum ('Pred  s) where reflectNum _ = (reflectNum (Proxy @ s)) - 1
instance ReflectNum s â ReflectNum ('Succ  s) where reflectNum _ = (reflectNum (Proxy @ s)) + 1
instance ReflectNum s â ReflectNum ('Twice s) where reflectNum _ = (reflectNum (Proxy @ s)) * 2

reifyIntegral â· (Integral a) â a â (â (s :: KNat). ReflectNum s â Proxy s -> w) â w
reifyIntegral i k = case quotRem i 2 of
  (0,0)  â k $ Proxy @ 'Zero
  (j,0)  â reifyIntegral j (\(p :: Proxy s) -> let n = reflectNum p in
                                               k $ Proxy @ ('Twice s) )
  (j,1)  â reifyIntegral j (\(_ :: Proxy s) -> k $ Proxy @ ('Succ('Twice s)))
  (j,-1) â reifyIntegral j (\(_ :: Proxy s) -> k $ Proxy @ ('Pred('Twice s)))

Zero 索引工作正常。

但第二个不能证明这一点 'Twice s 是 ReflectNum . 尽管如此,它也应该如此 s 反射数 因此 “两次 验证它,并且 k ,具有多态性 s 只要我们有证据证明 ReflectNum s

{-# LANGUAGE AllowAmbiguousTypes,GeneralizedNewtypeDeriving  #-}
{-# LANGUAGE  TypeFamilies, KindSignatures, FlexibleContexts #-}
{-# LANGUAGE TypeApplications, FunctionalDependencies, MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables , GADTs, MultiParamTypeClasses, RankNTypes                #-}
{-# LANGUAGE TypeOperators, UnicodeSyntax, DataKinds              #-}
{-# LANGUAGE UndecidableSuperClasses    #-}
module ImplicitConfigurationFirstPart where

import Data.Proxy

data KNat where
  Zero :: KNat
  Twice :: KNat -> KNat

class ReflectNum (s :: KNat) where reflectNum â· Num a â Proxy s -> a
instance                ReflectNum  'Zero      where reflectNum _ = 0
instance ReflectNum s â ReflectNum ('Twice s)  where reflectNum _ = (reflectNum (Proxy @ s)) * 2

reifyIntegral2 â· forall a w. (Integral a) â a â (â (s :: KNat). ReflectNum s â w) â w
reifyIntegral2 i k = case quotRem i 2 of
  (0,0)  â k @ 'Zero
  (j,0)  â reifyIntegral2 j k1

  where k1 :: forall (s :: KNat). ReflectNum s â w
        k1 = k @ ('Twice s)

1 回复 | 直到 6 年前

1

3

Alexis King 6 年前

但如果我们是 建筑物 一个多态值,除了一个类型的参数外,有没有办法绑定我们被调用的类型 Proxy s ?

接受一个类型参数,打算使用visible类型应用程序提供。这个问题的答案是使用 forall .

如果你有一些功能 f 书面使用例如

f :: Proxy s -> X -> Y

Proxy 通过启用 AllowAmbiguousTypes 和 ScopedTypeVariables 使用显式 福尔

{-# LANGUAGE AllowAmbiguousTypes, ScopedTypeVariables #-}
f :: forall s. X -> Y

这个 s F .