Part2_Sec5_3_3_dpair

Markdown generated from:
Source idr program: /src/Part2/Sec5_3_3_dpair.idr
Source lhs program: /src/Part2/Sec5_3_3_dpair.lhs

Section 5.3.3. Dependent Pair vs Haskell

Idris code example

module Part2.Sec5_3_3_dpair
import Data.Vect

{-
Note, Idris figures out Vect size.  
In Haskell "_" == "I do not care"  
In Idris "_" == "You figure it out"
-}
||| Conversion between a list and dependent pair
||| Think about using strong dependent types in runtime calculations.
listToVect : List a -> (n ** Vect n a)
listToVect [] = (_ ** [])
listToVect (x :: xs) = 
        let (_ ** vxs) = listToVect xs
        in (_ ** x :: vxs)

Compared to Haskell

Note, standard approach in Haskell is to use existential type (or GADT which gives equivalent functionality).
Typical name used in Haskell for this starts with 'Some'.

This follows the idea from 5.3.2 and naming convention from the book so instead of SomeVect I have VectUnknown

{-# LANGUAGE DeriveFunctor
   , StandaloneDeriving
   , GADTs
   , KindSignatures
   , DataKinds
   , TypeOperators 
   , ScopedTypeVariables
   , RankNTypes
#-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}

module Part2.Sec5_3_3_dpair where
import GHC.TypeLits
import Part2.Sec3_2_3_gen (Vect(..))

{-| 
 Provides link between Nat types and values. Often called Natty ('singletons' also calls it 'Sing n'.
 SNat allows to lift from value n to type n. And provides run time reflexion.
 Note: using predecessor (n - 1) instead of (1 + n) seems, in some cases, 
 to work better see Part2.Sec6_2_1_adder 
-}
data SNat (n :: Nat) where
 SZ :: SNat 0
 SS :: SNat n -> SNat (1 + n)

deriving instance Show (SNat n) 

{-| In Haskell, this would be typically called SomeVect -}
data VectUnknown a where 
   MkVect :: SNat n -> Vect n a -> VectUnknown a 
 
deriving instance Show a => Show (VectUnknown a) 

listToVect :: [a] -> VectUnknown a
listToVect [] = MkVect SZ VNil
listToVect (x : xs) = 
             let forXs = listToVect xs
             in case forXs of
             MkVect nx forXsV -> MkVect (SS nx) (x ::: forXsV) 

ghci:

*Part2.Sec5_3_3_dpair> listToVect [1,2,3]
MkVect (SS (SS (SS SZ))) (1 ::: (2 ::: (3 ::: VNil)))
*Part2.Sec5_3_3_dpair> 

A clear difference between Idris and Haskell is that Idris figures out the size (_) and I have to type it in Haskell.

There is also a CPS approach, singletons library uses it, (it uses RankNTypes). For Vect type I can define:

withVectUnknown :: VectUnknown a -> (forall n . SNat n -> Vect n a -> r) -> r
withVectUnknown (MkVect n v) f = f n v

withListAsVect :: [a] -> (forall n . SNat n -> Vect n a -> r) -> r 
withListAsVect list f = withVectUnknown (listToVect list) f

test = withListAsVect [1,2,3] $ \n vect -> show vect

This is similar to withNat, withSomeNat I created in /src/Util/NonLitsNatAndVector.hs

ghci:

*Part2.Sec5_3_3_dpair> test
"1 ::: (2 ::: (3 ::: VNil))"