[Haskell-cafe] type level Min function for GHC.TypeLits?

[Baojun Wang]

Hi Cafe,

I'm trying to do some basic type level tricks, I wonder whether it is
possible to get ``vZipWith`` in below code snippet working:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

import GHC.TypeLits
import Data.Proxy

data Vect :: (Nat -> * -> *) where
  VNil :: Vect 0 a
  VCons :: a -> Vect n a -> Vect (1+n) a

deriving instance (Show a) => Show (Vect n a)

vlength :: forall n a . KnownNat n => Vect n a -> Integer
vlength _ = natVal (Proxy :: Proxy n)

vconcat :: Vect n a -> Vect m a -> Vect (n+m) a         -- Need type
checker plugin
vconcat VNil ys = ys
vconcat xs VNil = xs
vconcat (VCons x xs) ys = VCons x (vconcat xs ys)

type family Min3 (t :: Bool) (m :: Nat) (n :: Nat) :: Nat

type instance Min3 'True m n = m
type instance Min3 'False m n = n
type Min m n = Min3 (m <=? n) m n

vZipWith :: (a -> b -> c) -> Vect m a -> Vect n b -> Vect (Min m n) c
vZipWith f VNil _ = VNil
vZipWith f _ VNil = VNil
vZipWith f (VCons x xs) (VCons y ys) = f x y `VCons` vZipWith f xs ys


As I got errors:

/home/wangbj/downloads/stack/vect/src/Vect.hs:51:21:
    Could not deduce (Min3 (m <=? 0) m 0 ~ 0)
    from the context (n ~ 0)
      bound by a pattern with constructor
                 VNil :: forall a. Vect 0 a,
               in an equation for ‘vZipWith’
      at /home/wangbj/downloads/stack/vect/src/Vect.hs:51:14-17
    Expected type: Vect (Min m n) c
      Actual type: Vect 0 c
    Relevant bindings include
      vZipWith :: (a -> b -> c)
                  -> Vect m a -> Vect n b -> Vect (Min m n) c
        (bound at /home/wangbj/downloads/stack/vect/src/Vect.hs:50:1)
    In the expression: VNil
    In an equation for ‘vZipWith’: vZipWith f _ VNil = VNil

/home/wangbj/downloads/stack/vect/src/Vect.hs:52:40:
    Could not deduce (Min3 (m <=? n) m n
                      ~ (1 + Min3 (n1 <=? n2) n1 n2))
    from the context (m ~ (1 + n1))
      bound by a pattern with constructor
                 VCons :: forall a (n :: Nat). a -> Vect n a -> Vect (1 +
n) a,
               in an equation for ‘vZipWith’
      at /home/wangbj/downloads/stack/vect/src/Vect.hs:52:13-22
    or from (n ~ (1 + n2))
      bound by a pattern with constructor
                 VCons :: forall a (n :: Nat). a -> Vect n a -> Vect (1 +
n) a,
               in an equation for ‘vZipWith’
      at /home/wangbj/downloads/stack/vect/src/Vect.hs:52:26-35
    Expected type: Vect (Min m n) c
      Actual type: Vect (1 + Min n1 n2) c
    Relevant bindings include
      ys :: Vect n2 b
        (bound at /home/wangbj/downloads/stack/vect/src/Vect.hs:52:34)
      xs :: Vect n1 a
        (bound at /home/wangbj/downloads/stack/vect/src/Vect.hs:52:21)
      vZipWith :: (a -> b -> c)
                  -> Vect m a -> Vect n b -> Vect (Min m n) c
        (bound at /home/wangbj/downloads/stack/vect/src/Vect.hs:50:1)
    In the expression: f x y `VCons` vZipWith f xs ys
    In an equation for ‘vZipWith’:
        vZipWith f (VCons x xs) (VCons y ys)
          = f x y `VCons` vZipWith f xs ys
Failed, modules loaded: none.

Also I tried https://github.com/yav/type-nat-solver but got error like:

*** Exception: user error (Unexpected result from the SMT solver:
  Expected: success
  Result: (error "line 57 column 16: unknown constant tn_0" )

Which I have no idea what it really means.

Is there any way to get ``vZipWith`` working without too much hassle?

Thanks
baojun
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160701/7089def8/attachment.html>