I'm trying to understand how to use GADT types to simulate dependent
types. I'm trying to write a version of list that uses Peano numbers
in the types to keep track of how many elements are in the list. Like this:
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module Plist whe
Am Samstag, 28. Juni 2008 19:51 schrieb Paul Johnson:
> I'm trying to understand how to use GADT types to simulate dependent
> types. I'm trying to write a version of list that uses Peano numbers
> in the types to keep track of how many elements are in the list. Like
> this:
>
> {-# OPTIONS -fgl
On Saturday 28 June 2008, Paul Johnson wrote:
> I'm trying to understand how to use GADT types to simulate dependent
> types. I'm trying to write a version of list that uses Peano numbers
> in the types to keep track of how many elements are in the list. Like
> this:
>
> {-# OPTIONS -fglasgow-ex
Daniel Fischer wrote:
My Oleg rating isn't high either, and certainly you can do it more elegant,
but
class Concat l1 l2 l3 | l1 l2 -> l3, l1 l3 -> l2 where
pConcat :: l1 a -> l2 a -> l3 a
instance Concat (Plist Zero) (Plist n) (Plist n) where
pConcat _ ys = ys
instance Concat (Pli
