I started reading Chapter 6 of "Type-driven development with Idris" and attempted to write a smart constructor for a tupled vector.
TupleVect : Nat -> Type -> Type
TupleVect Z _ = ()
TupleVect (S k) a = (a, TupleVect k a)
someValue : TupleVect 4 Nat
someValue = (1,2,3,4,())
TupleVectConstructorType : Nat -> Type -> Type
TupleVectConstructorType n typ = helper n
where
helper : Nat -> Type
helper Z = TupleVect n typ
helper (S k) = typ -> helper k
tupleVect : (n : Nat) -> (a : Type) -> TupleVectConstructorType n a
tupleVect Z a = ()
tupleVect (S Z) a = \val => (val, ())
tupleVect (S (S Z)) a = \val2 => \val1 => (val2, val1, ())
-- ??? how to create tupleVect (S k) a
How to create a constructor for an arbitrary k?
Basically @Matthias Berndt's idea. Counting down the arrows to be added, while making the final tuple longer. For this we need to access the more permissive helper from TupleVectType
.
TupleVectType' : Nat -> Nat -> Type -> Type
TupleVectType' Z n a = TupleVect n a
TupleVectType' (S k) n a = a -> TupleVectType' k (S n) a
TupleVectType : Nat -> Type -> Type
TupleVectType n = TupleVectType' n Z
tupleVect : (n : Nat) -> (a : Type) -> TupleVectType n a
tupleVect n a = helper n Z a ()
where
helper : (k, n : Nat) -> (a : Type) -> (acc : TupleVect n a)
-> TupleVectType' k n a
helper Z n a acc = acc
helper (S k) n a acc = \x => helper k (S n) a (x, acc)
someValue2 : TupleVect 4 Nat
someValue2 = (tupleVect 4 Nat) 4 3 2 1
Though note that this will result in \v2 => \v1 => (v1, v2, ())
and not \v2 => \v1 => (v2, v1, ())
as the former fits the recursive definition of TupleVect (S k) a = (a, TupleVect k a)
better.
I know almost nothing about Idris except that it's a dependently-typed, Haskell-like language. But I find this problem intriguing, so I gave it a shot.
Clearly you need a recursive solution here. My idea is to use an additional parameter f
which accumulates the val1
..val_n
parameters that the function has eaten so far. When the base case is reached, f
is returned.
tupleVectHelper Z a f = f
tupleVectHelper (S n) a f = \val => tupleVectHelper n a (val, f)
tupleVect n a = tupleVectHelper n a ()
I have no idea if this works, and I haven't yet figured out how to write the type of tupleVectHelper
, but I've tried doing the substitutions manually for n = 3
and it does seem to work out on paper, though the resulting tuple is backwards. But I think that shouldn't be too hard to fix.
Hope this helps!
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With