时间戳

首页 > 解决方案 > 将 Haskell 函数“分解”为具有各种中间类型的两个函数时如何避免重复？

haskell - 将 Haskell 函数“分解”为具有各种中间类型的两个函数时如何避免重复？

问题描述

考虑以下 Haskell 代码：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}

import Data.Singletons.TH

singletons [d| data SimpleType = Aaa | Bbb | Ccc | Ddd
                                 deriving (Read)
             |]

-- each SimpleType value has an associated type
type family Parsed (t :: SimpleType) :: * where
  Parsed Aaa = [Int]
  Parsed Bbb = Maybe Int
  Parsed Ccc = (Int, Int)
  Parsed Ddd = Int

forth :: SSimpleType t -> Int -> Parsed t
forth SAaa x = [x,x*2,x*3]
forth SBbb x = Just x
forth SCcc x = (1337, x)
forth SDdd x = x

back :: SSimpleType t -> Parsed t -> Int
back SAaa [_, y, _] = y + 5
back SBbb (Just y) = y - 7
back SCcc (y1, y2) = y1 + y2
back SDdd y = y * 2

helper b = back b . forth b

go :: SimpleType -> Int -> Int
go Aaa = helper SAaa
go Bbb = helper SBbb
go Ccc = helper SCcc
go Ddd = helper SDdd

main = do
  -- SimpleType value comes at run-time
  val <- readLn
  putStrLn $ show $ go val 100

定义时是否可以避免重复go？换句话说，有没有办法写出类似的东西：

go val = helper (someMagicFunction val)

标签： haskelldependent-type

解决方案

您可以使用toSingfromSingKind将 的值转换为SimpelType的值SomeSing SimpleType，这是对 的存在量化包装Sing SimpleType。然后，您可以打开该值以获得 get Sing SimpleType，然后您可以将其传递给backand forth：

go :: SimpleType -> Int -> Int
go val x =
  case toSing val of
    SomeSing s -> back s $ forth s x

您正在使用的拼接会SingKind为您（以及许多其他事情）生成一个实例。singletons

请注意，虽然单分支case要求成为 a let，但这不会编译：

go val x =
  let (SomeSing s) = toSing val
  in back s $ forth s x

这是被禁止的，因为let它可能是递归的，并且由于解包 GADT 可能会将新类型带入上下文，它可能会导致创建无限类型。另一方面，case分支不能递归，所以这是可行的。（此解释归功于@HTNW）

但是辅助函数也可以工作：

go val x = helper $ toSing val
    where
      helper (SomeSing s) = back s $ forth s x

推荐阅读